#!/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=/usr/proj/isabelle-repository/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 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)!

    * 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 -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

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

# 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 \) \) \

  | grep -v 'gfx/.*pdf')

mv -f $MOVE Distribution/doc

rm Distribution/doc/Isa-logics.eps

cp Admin/index.html $DISTBASE

rm -rf Admin Doc

mkdir src

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/index1.html lib/html/index2.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

# 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; )

UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ]

gzip $DISTNAME.tar

gzip ${DISTNAME}_pdf.tar

PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ]

PACKED_SIZE_PDF=$[ $(wc -c <${DISTNAME}_pdf.tar.gz) / 1024 ]

# prepare dist index.html

perl -pi -e \

 "s/{ISABELLE}/$DISTNAME/g; \

  s/{PACKED_SIZE}/$PACKED_SIZE/g; \

  s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g; \

  s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \

  s/{AUTHOR}/$LOGNAME/g; \

  s/{DATE}/$DATE/g;" \

    index.html

# final note

echo

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

echo