#!/usr/bin/env bash

 #

 # $Id$

 #

 # makedist -- make Isabelle source distribution.

 ## global settings

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

 SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools ZF"

 export CVSROOT=/usr/proj/isabelle-repository/archive

 [ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@atbroy100.informatik.tu-muenchen.de:$CVSROOT"

 umask 022

 ## executables

 TAR=tar

 type -path gtar >/dev/null && TAR=gtar

 FIND=find

 type -path gfind >/dev/null && FIND=gfind

 [ -z "$CVS2CL" ] && type -path cvs2cl && CVS2CL=cvs2cl

 #paranoia setting for sunbroy

 PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH"

 PATH="/home/scala/bin:$PATH"

 ## diagnostics

 PRG=$(basename "$0")

 THIS=$(cd $(dirname "$0"); echo "$PWD")

 function usage()

 {

   cat <<EOF

 Usage: $PRG VERSION [NAME]

   Make Isabelle distribution from the master sources at TUM.

   VERSION may be either a tag like "IsabelleXXXX" that specifies the

   release to be exported from the repository, or "-" to checkout the

   current sources as an unofficial release.

   NAME specifies an explicit distribution name, by default it is

   derived from VERSION.

   Checklist for official releases (before running this script):

     * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.

     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.

     * Tag the current repository version, e.g.:

         cvs -d /home/isabelle-repository/archive rtag IsabelleXXXX isabelle

       PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!

    After running this script:

     * Symlink generated files in website/ directory to their appropriate

       places in the isabelle website sources.

 EOF

   exit 1

 }

 function fail()

 {

   echo "$1" >&2

   exit 2

 }

 ## process command line

 [ "$#" -ne 1 -a "$#" -ne 2 ] && usage

 VERSION="$1"; shift

 if [ "$#" -eq 0 ]; then

   DISTNAME=""

 else

   DISTNAME="$1"; shift

 fi

 ## main

 # dist version

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

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

 if [ "$VERSION" = "-" ]; then

   DISTIDENT="Isabelle_$DATE"

   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"

   DISTVERSION="$DISTNAME"

   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"

   UNOFFICIAL=true

 else

   DISTIDENT="$VERSION"

   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"

   DISTVERSION="$DISTNAME: $DISTDATE"

   EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"

   UNOFFICIAL=""

 fi

 DISTBASE="$DISTPREFIX/dist-$DISTNAME"

 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"

 [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"

 [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"

 # export repository

 echo "###"

 echo "### Exporting $DISTIDENT ..."

 echo "###"

 cd "$DISTBASE"

 $EXPORT || fail "Export failed!"

 if [ -n "$CVS2CL" ]; then

   cd $DISTNAME

   $CVS2CL

   gzip ChangeLog

   cp ChangeLog.gz ..

   cd ..

 fi

 $FIND . -name CVS -print | xargs rm -rf

 $FIND . -name .cvsignore -print | xargs rm -rf

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

 $FIND . -print | xargs chmod u+rw

 # build docs

 echo "###"

 echo "### Building docs ..."

 echo "###"

 cd "$DISTBASE/$DISTNAME/Doc"

 PDFLATEX=$(type -path pdflatex)

 for DOC in $(cat Contents)

 do

   pushd "$DOC" > /dev/null

   make dvi || fail "DVI document for $DOC failed!"

   { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"

   popd

 done

 # prepare dist dir for release

 echo "###"

 echo "### Preparing distribution ..."

 echo "###"

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

 mkdir -p ../website

 cat > ../website/distinfo.mak <<EOF

 # this is a generated file - do not edit unless you know what you are doing!

 DISTNAME=$DISTNAME

 DISTIDENT=$DISTIDENT

 DISTBASE=$DISTBASE

 EOF

 cp Distribution/lib/html/library_index_content.template ../website/

 MOVE=$($FIND Doc \( -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 Distribution/doc

 rm Distribution/doc/Isa-logics.eps

 rm -rf Doc

 mkdir src contrib

 mv $SRCS src

 mv Distribution/* .

 rmdir Distribution

 ( cd lib/browser; make; ) || fail "Failed to build graph browser!"

 ( cd lib/classes; ./mk; )

 [ -f lib/classes/isabelle.jar ] || fail "Failed to build Isabelle process wrapper!"

 if type -p scalac >/dev/null

 then

   ( cd lib/jedit/plugin; ./mk; )

   [ -f lib/jedit/isabelle.jar ] || fail "Failed to build jEdit plugin!"

 else

   echo "Warning: Scala unavailable -- skipping jEdit plugin"

 fi

 cp doc/isabelle*.eps lib/logo

 if [ -n "$UNOFFICIAL" ]; then

   {

     echo

     echo "IMPORTANT NOTE"

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

     echo

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

     echo

   } >ANNOUNCE

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

 fi

 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/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version

 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README

 ( cd src; ../Admin/maketags; )

 rm -rf Admin

 rm -f TODO

 # create archive

 echo "###"

 echo "### Creating archives ..."

 echo "###"

 cd "$DISTBASE"

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

 rm -f Isabelle

 ln -s "$DISTNAME" Isabelle

 chown -R "$LOGNAME" "$DISTNAME"

 chmod -R u+w "$DISTNAME"

 chmod -R g=o "$DISTNAME"

 chgrp -R isabelle "$DISTNAME" Isabelle

 mkdir -p "pdf/$DISTNAME/doc"

 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"

 sync; sleep 3

 echo "$DISTNAME.tar.gz"

 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"

 gzip "$DISTNAME.tar"

 echo "${DISTNAME}_pdf.tar.gz"

 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )

 gzip "${DISTNAME}_pdf.tar"

 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"

 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf

 # cleanup dist

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

 mkdir "$DISTNAME"

 mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${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"

 chgrp -R isabelle "$DISTNAME"

 rm -rf "${DISTNAME}-old"

 # final note

 echo "###"

 echo "### Finished makedist."

 echo "###"