#!/bin/bash

 #

 # $Id$

 #

 # makedist -- make Isabelle distribution.

 ## global settings

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

 CVSROOT=/isabelle/archive

 DISTBASE=~/tmp/isadist

 ## diagnostics

 PRG=$(basename $0)

 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 that README files are up to date (should have Id: lines).

     * Check that Pure/ROOT.ML/version is up to date!

     * Check release name and date in NEWS!

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

     * Make sure that the repository version of Doc is consistent

       (watch out for *.bbl, *.rao, *.ind)!

     * Check ML_SYSTEM defaults!

 EOF

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

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

     cat <<EOF

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

         cvs 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")

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

   DISTNAME=Isabelle_$DATE

   EXPORT="checkout"

   UNOFFICIAL=true

 else

   DISTNAME="$VERSION"

   EXPORT="export -r $VERSION"

   UNOFFICIAL=""

 fi

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

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

 # export from repository

 echo

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

 echo

 cd $DISTBASE

 export CVSROOT

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

 # make docs

 cd $DISTBASE/$DISTNAME/Doc

 for DOC in $(cat Contents)

 do

   cd $DOC

   make dist

   cd ..

 done

 # prepare dist dir for release

 cd $DISTBASE/$DISTNAME

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

 mkdir -p Tools/8bit/bin    #FIXME tmp

 find Doc -name \*.dvi -o -name \*.eps -o -name \*.ps -exec mv {} Distribution/doc \;

 rm -rf Admin Doc

 mkdir src

 mv $LOGICS src

 mv index.html src

 mv Distribution/* .

 rmdir Distribution

 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

 lynx -dump README.html >README

 # create archive

 cd $DISTBASE

 #FIXME sometimes doesn't work!?

 chown -R $LOGNAME:isabelle $DISTNAME

 chmod -R u+w $DISTNAME

 chmod -R g+w $DISTNAME

 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz

 # final note

 echo

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

 echo