#!/usr/bin/env bash

 #

 # makedist -- make Isabelle source distribution

 ## global settings

 REPOS_NAME="${REPOS_NAME:-isabelle}"

 REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}"

 DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}"

 umask 022

 ## diagnostics

 PRG="$(basename "$0")"

 THIS="$(cd $(dirname "$0"); pwd)"

 function usage()

 {

   cat <<EOF

 Usage: $PRG [OPTIONS] [VERSION]

   Options are:

     -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component

     -r RELEASE         proper release with name"

   Make Isabelle distribution from the main Mercurial repository at TUM.

   VERSION identifies the snapshot, using usual Mercurial terminology;

   the default is RELEASE if given, otherwise "tip".

 EOF

   exit 1

 }

 function fail()

 {

   echo "$1" >&2

   exit 2

 }

 ## process command line

 # options

 RELEASE=""

 ISABELLE_JEDIT_BUILD_HOME=""

 while getopts "j:r:" OPT

 do

   case "$OPT" in

     j)

       ISABELLE_JEDIT_BUILD_HOME="$OPTARG"

       ;;

     r)

       RELEASE="$OPTARG"

       ;;

     \?)

       usage

       ;;

   esac

 done

 shift $(($OPTIND - 1))

 # args

 VERSION=""

 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }

 [ -z "$VERSION" ] && VERSION="$RELEASE"

 [ -z "$VERSION" ] && VERSION="tip"

 [ "$#" -gt 0 ] && usage

 ## main

 # tmp

 TMP="tmp-$USER$$"

 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }

 # retrieve archive and resolve version identifier

 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"

 cd "$DISTPREFIX/$TMP"

 echo "###"

 echo "### Retrieving Mercurial repository $VERSION"

 echo "###"

 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \

   fail "Failed to retrieve $VERSION"

 IDENT=$(echo * | sed "s/${REPOS_NAME}-//")

 rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"

 rm -f "${REPOS_NAME}-${IDENT}/.hgtags"

 rm -f "${REPOS_NAME}-${IDENT}/.hgignore"

 rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"

 # dist name

 DATE=$(env LC_ALL=C date "+%d-%b-%Y")

 DISTDATE=$(env LC_ALL=C date "+%B %Y")

 if [ -z "$RELEASE" ]; then

   DISTNAME="Isabelle_$DATE"

   DISTVERSION="Isabelle repository snapshot $IDENT $DATE"

 else

   DISTNAME="$RELEASE"

   DISTVERSION="$DISTNAME: $DISTDATE"

 fi

 DISTBASE="$DISTPREFIX/dist-$DISTNAME"

 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }

 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }

 cd "$DISTBASE"

 mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"

 purge_tmp

 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"

 # prepare dist for release

 echo "###"

 echo "### Preparing distribution $DISTNAME"

 echo "###"

 rm -f .hgignore

 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x

 find . -print | xargs chmod -f u+rw

 ./Admin/build all || fail "Failed to build distribution"

 if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then

   [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""

   eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"

   [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"

   export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION

   ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"

 fi

 rm -rf Admin

 MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')

 mv -f $MOVE doc

 rm doc/Isa-logics.eps

 rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf

 rm -rf doc-src

 mkdir -p contrib

 cat >contrib/README <<EOF

 This directory contains add-on components that contribute to the main

 Isabelle distribution.  Separate licensing conditions apply, see each

 directory individually.

 EOF

 cp doc/isabelle*.eps lib/logo

 if [ -z "$RELEASE" ]; then

   {

     echo

     echo "IMPORTANT NOTE"

     echo "=============="

     echo

     echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."

     echo "See $REPOS/log/$IDENT for details."

     echo

   } >ANNOUNCE

 else

   perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML

 fi

 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML

 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings

 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings

 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template

 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version

 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README

 # create archive

 echo "###"

 echo "### Creating archive ..."

 echo "###"

 cd "$DISTBASE"

 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST

 echo "$IDENT" >../ISABELLE_IDENT

 chown -R "$LOGNAME" "$DISTNAME"

 chmod -R u+w "$DISTNAME"

 chmod -R g=o "$DISTNAME"

 chgrp -R isabelle "$DISTNAME"

 echo "$DISTNAME.tar.gz"

 tar -czf "$DISTNAME.tar.gz" "$DISTNAME"

 # cleanup dist

 mv "$DISTNAME" "${DISTNAME}-old"

 mkdir "$DISTNAME"

 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \

   "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"

 mkdir "$DISTNAME/doc"

 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"

 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle

 chgrp -R isabelle "$DISTNAME"

 rm -rf "${DISTNAME}-old"

 echo "DONE"