#!/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 -P"

  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 -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 {} \;

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

rm Distribution/doc/Isa-logics.eps

rm -rf Admin Doc

mkdir src

mv $LOGICS src

mv Distribution/* .

rmdir Distribution

( cd lib/browser; make; )

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