#!/bin/bash

 #

 # $Id$

 #

 # makedist -- make Isabelle distribution.

 ## global settings

 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF"

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

 DISTPREFIX=~/tmp/isadist

 umask 022

 TAR=tar

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

 FIND=find

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

 ## diagnostics

 PRG=$(basename "$0")

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

 function usage()

 {

   echo "###"

   echo "### Usage: $PRG VERSION"

   echo "###"

   cat <<EOF

   Make Isabelle distribution from the master sources at TUM.

   VERSION may be either a tag like "Isabelle99-XX" that specifies the

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

   current sources as an unofficial release, or "--" to produce a

   tentative release from the present copy of the Isabelle repository.

   Checklist for official releases (before running this script):

     * Check release name and date in NEWS!

     * Check that README files are up to date (should have Id: lines).

     * Check Admin/index.html.

 EOF

   #Wicked! We just won't tell other users ...

   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then

     cat <<EOF

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

         cvs -d $CVSROOT rtag Isabelle99-XX isabelle

       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!

 EOF

   fi

   cat <<EOF

   After the distribution has been created succesfully, you might want

   to run some makeall tests using different ML systems.

 EOF

   exit 1

 }

 function fail()

 {

   echo "$1" >&2

   exit 2

 }

 ## process command line

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

 VERSION="$1"

 shift

 ## main

 # dist version

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

 DISTDATE=$(date "+%B %Y")

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

   DISTNAME="Isabelle_$DATE"

   DISTVERSION="$DISTNAME"

   EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"

   UNOFFICIAL="unofficial test"

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

   DISTNAME="Isabelle_$DATE"

   DISTVERSION="$DISTNAME"

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

   UNOFFICIAL="unofficial"

 else

   DISTNAME="$VERSION"

   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 $DISTNAME ..."

 echo "###"

 cd "$DISTBASE"

 $EXPORT

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

 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf

 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf

 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf

 # build docs

 echo "###"

 echo "### Building docs ..."

 echo "###"

 cd "$DISTBASE/$DISTNAME/Doc"

 PDFLATEX=$(type -path pdflatex)

 for DOC in $(cat Contents)

 do

   cd "$DOC"

   make dvi

   [ -n "$PDFLATEX" ] && make clean pdf

   cd ..

 done

 # prepare dist dir for release

 echo "###"

 echo "### Preparing distribution ..."

 echo "###"

 cd "$DISTBASE/$DISTNAME"

 cp -R Admin/page ..

 cp Distribution/doc/Contents ../page

 cp Distribution/lib/logo/isabelle.gif ../page/main-content

 cp Distribution/lib/logo/isabelle.gif ../page/dist-content

 echo "$DISTNAME" > ../page/DISTNAME

 MOVE=$($FIND Doc \( -type f -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 Tools

 mkdir src contrib

 mv $LOGICS src

 mv Distribution/* .

 rmdir Distribution

 ( cd lib/browser; make; )

 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

 fi

 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html

 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML

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

 lynx -dump README.html >README

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

 rm -rf Admin

 # create archive

 echo "###"

 echo "### Creating archives ..."

 echo "###"

 cd "$DISTBASE"

 rm -f Isabelle

 ln -s "$DISTNAME" Isabelle

 chown -R "$LOGNAME" "$DISTNAME"

 chgrp -R isabelle "$DISTNAME"

 chmod -R u+w "$DISTNAME"

 chmod -R g=o "$DISTNAME"

 mkdir -p "pdf/$DISTNAME/doc"

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

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

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

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

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

 gzip "$DISTNAME.tar"

 gzip "${DISTNAME}_pdf.tar"

 # cleanup dist

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

 mkdir "$DISTNAME"

 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" "$DISTNAME"

 mkdir "$DISTNAME/doc"

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

 chgrp -R isabelle "$DISTNAME"

 rm -rf "${DISTNAME}-old"

 # final note

 echo "###"

 echo "### Finished."

 echo "###"