#!/usr/bin/env bash

#

# makedist -- make Isabelle source distribution

## global settings

REPOS_NAME="isabelle-release"

REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"

DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"

umask 022

## diagnostics

PRG="$(basename "$0")"

THIS="$(cd $(dirname "$0"); pwd)"

function usage()

{

  cat <<EOF

Usage: $PRG [OPTIONS] [VERSION]

  Options are:

    -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component

    -r RELEASE         proper release with name"

  Make Isabelle distribution from the main Mercurial repository at TUM.

  VERSION identifies the snapshot, using usual Mercurial terminology;

  the default is RELEASE if given, otherwise "tip".

EOF

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

## process command line

# options

RELEASE=""

ISABELLE_JEDIT_BUILD_HOME=""

while getopts "j:r:" OPT

do

  case "$OPT" in

    j)

      ISABELLE_JEDIT_BUILD_HOME="$OPTARG"

      ;;

    r)

      RELEASE="$OPTARG"

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

# args

VERSION=""

[ "$#" -gt 0 ] && { VERSION="$1"; shift; }

[ -z "$VERSION" ] && VERSION="$RELEASE"

[ -z "$VERSION" ] && VERSION="tip"

[ "$#" -gt 0 ] && usage

## main

# tmp

TMP="tmp-$USER$$"

function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }

# retrieve archive and resolve version identifier

mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"

cd "$DISTPREFIX/$TMP"

echo "###"

echo "### Retrieving Mercurial repository $VERSION"

echo "###"

if expr match "$REPOS" "https\?://" > /dev/null

then

  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \

    fail "Failed to retrieve $VERSION"

else

  { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \

    fail "Failed to retrieve $VERSION"

fi

IDENT=$(echo * | sed "s/${REPOS_NAME}-//")

rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"

rm -f "${REPOS_NAME}-${IDENT}/.hgtags"

rm -f "${REPOS_NAME}-${IDENT}/.hgignore"

rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"

# dist name

DATE=$(env LC_ALL=C date "+%d-%b-%Y")

DISTDATE=$(env LC_ALL=C date "+%B %Y")

if [ -z "$RELEASE" ]; then

  DISTNAME="Isabelle_$DATE"

  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"

else

  DISTNAME="$RELEASE"

  DISTVERSION="$DISTNAME: $DISTDATE"

fi

DISTBASE="$DISTPREFIX/dist-$DISTNAME"

mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }

[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }

cd "$DISTBASE"

mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"

purge_tmp

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

# prepare dist for release

echo "###"

echo "### Preparing distribution $DISTNAME"

echo "###"

rm -f .hgignore

find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x

find . -print | xargs chmod -f u+rw

perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings

./Admin/build all || fail "Failed to build distribution"

if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then

  [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""

  eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"

  [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"

  export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION

  ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"

fi

rm -rf Admin

MOVE=$(find doc-src \( -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 doc

rm doc/Isa-logics.eps

rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf

rm -rf doc-src

mkdir -p contrib

cat >contrib/README <<EOF

This directory contains add-on components that contribute to the main

Isabelle distribution.  Separate licensing conditions apply, see each

directory individually.

EOF

cp doc/isabelle*.eps lib/logo

if [ -z "$RELEASE" ]; then

  {

    echo

    echo "IMPORTANT NOTE"

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

    echo

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

    echo "See $REPOS/log/$IDENT for details."

    echo

  } >ANNOUNCE

else

  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML

fi

perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML

perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings

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,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version

perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README

# create archive

echo "###"

echo "### Creating archive ..."

echo "###"

cd "$DISTBASE"

echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST

echo "$IDENT" >../ISABELLE_IDENT

chown -R "$LOGNAME" "$DISTNAME"

chmod -R u+w "$DISTNAME"

chmod -R g=o "$DISTNAME"

chgrp -R isabelle "$DISTNAME"

echo "$DISTNAME.tar.gz"

tar -czf "$DISTNAME.tar.gz" "$DISTNAME"

# cleanup dist

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

mkdir "$DISTNAME"

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

rm -f Isabelle && ln -sf "$DISTNAME" Isabelle

chgrp -R isabelle "$DISTNAME"

rm -rf "${DISTNAME}-old"

echo "DONE"