#!/bin/bash

 #

 # $Id$

 #

 # makedist -- make Isabelle distribution.

 ## global settings

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

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

 DISTPREFIX=~/tmp/isadist

 ## 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 "Isabelle94-XX" that specifies the

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

   current sources as an unofficial release.

   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.

     * Make sure that encoding info is consistent (fixencoding)!

     * Check ML_SYSTEM defaults!

 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 Isabelle94-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="checkout -P"

   UNOFFICIAL=true

 else

   DISTNAME="$VERSION"

   DISTVERSION="$DISTNAME: $DISTDATE"

   EXPORT="export -r $VERSION"

   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 from repository

 echo

 echo "Exporting $DISTNAME from repository. Please be patient ..."

 echo

 cd $DISTBASE

 export CVSROOT

 cvs -f -q $EXPORT -d $DISTNAME isabelle

 find . -name CVS -exec rm -rf {} \;

 # make docs

 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

 # make WWW pages

 export DISTNAME

 (cd $DISTBASE/$DISTNAME/Admin/page; make clean; make dist; cd dist; cp * $DISTBASE)

 # prepare dist dir for release

 cd $DISTBASE/$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

   } >UNOFFICIAL

 fi

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

 perl -pi -e "s/Isabelle repository/$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

 cd $DISTBASE

 chown -R $LOGNAME:isabelle $DISTNAME

 chmod -R u+w $DISTNAME

 TAR=tar

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

 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/lib/logo/isabelle.gif .

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

 mkdir $DISTNAME/doc && \

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

 rm -rf ${DISTNAME}-old

 # prepare web pages

 #FIXME

 #$THIS/filesizes -norpm

 # final note

 echo

 echo "That's it. You'll find the distribution in $DISTBASE."

 echo