#!/usr/bin/env bash

 #

 # $Id$

 #

 # makedist -- make Isabelle source distribution.

 ## global settings

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

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

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

 [ ! -d "$CVSROOT" ] && CVSROOT="sunbroy2.informatik.tu-muenchen.de:$CVSROOT"

 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()

 {

   cat <<EOF

 Usage: $PRG VERSION [NAME]

   Make Isabelle distribution from the master sources at TUM.

   VERSION may be either a tag like "Isabelle2005" 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 Admin/website contents.

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

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

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

         cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle2005 isabelle

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

 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=$(date "+%d-%b-%Y")

 DISTDATE=$(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="unofficial"

 else

   DISTIDENT="$VERSION"

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

   DISTVERSION="$DISTNAME: $DISTDATE"

   EXPORT="cvs -f -q export -P -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

   mv 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

 # 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 || fail "DVI document for $DOC failed!"

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

   cd ..

 done

 # prepare dist dir for release

 echo "###"

 echo "### Preparing distribution ..."

 echo "###"

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

 cp -R Admin/website ..

 mkdir -p ../website/conf

 cat > ../website/conf/distname.mak <<EOF

 # this is a generated file - do not edit!

 DISTNAME=$DISTNAME

 DISTIDENT=$DISTIDENT

 EOF

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

 mkdir src contrib

 mv $LOGICS src

 mv Distribution/* .

 rmdir Distribution

 ( cd lib/browser; make; ) || fail "Graph browser build failed!"

 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 lib/Tools/version

 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

 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"

 #~ page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index"

 #~ cat > "pdf/$DISTNAME/doc/index.html" <<EOF

 #~ <html>

 #~ <head>

 #~ <title>$DISTNAME Documentation</title>

 #~ </head>

 #~ <body>

 #~ <h1>$DISTNAME Documentation</h1>

 #~ $(cat "pdf/$DISTNAME/doc/index")

 #~ </body>

 #~ </html>

 #~ EOF

 #~ rm "pdf/$DISTNAME/doc/index"

 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 "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc"

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

 # cleanup dist

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

 mkdir "$DISTNAME"

 mv "${DISTNAME}-old/README.html" "${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/index.html" "$DISTNAME/doc"

 chgrp -R isabelle "$DISTNAME"

 rm -rf "${DISTNAME}-old"

 # final note

 echo "###"

 echo "### Finished makedist."

 echo "###"