#!/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=/home/isabelle-repository/archive

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

 [ -z "$CVS2CL" ] && type -path cvs2cl >/dev/null && CVS2CL=cvs2cl

 umask 022

 ## 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.

 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" -a -n "$UNOFFICIAL" ]; 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 components

 "$DISTBASE/$DISTNAME/Admin/build" all || fail "Failed to build distribution"

 # 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 Distribution/doc/codegen_process.pdf

 rm -rf Doc

 mkdir src contrib

 mv $SRCS src

 mv Distribution/* .

 rmdir Distribution

 cp doc/isabelle*.eps lib/logo

 if [ -n "$UNOFFICIAL" ]; then

   {

     echo

     echo "IMPORTANT NOTE"

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

     echo

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

     echo

   } >ANNOUNCE

 else

   perl -pi -e "s/val is_official = false/val is_official = true/" 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

 rm -rf Admin

 # 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"

 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"

 echo "###"

 echo "### Finished makedist."

 echo "###"