Admin/makedist_mercurial

make Isabelle source distribution (via Mercurial);

#!/usr/bin/env bash
#
# $Id$
#
# makedist_mercurial -- make Isabelle source distribution (via Mercurial)

## global settings

REPOS="http://isabelle.in.tum.de/isabelle-bin/mercurial.cgi"

DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
TMP="tmp-$USER$$"

umask 022


## diagnostics

PRG=$(basename "$0")
THIS=$(cd $(dirname "$0"); echo "$PWD")

function usage()
{
  cat <<EOF

Usage: $PRG [OPTIONS] [VERSION]

  Options are:
    -r NAME         proper release with name"

  FIXME 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

# options

RELEASE=""

while getopts "r:" OPT
do
  case "$OPT" in
    r)
      RELEASE="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

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

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


## main

# retrieve archive and resolve version identifier

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

echo "###"
echo "### Retrieving $REPOS/archive/${VERSION}.tar.gz"
echo "###"

{ wget -q "$REPOS/archive/${VERSION}.tar.gz" && tar -x -z -f "${VERSION}.tar.gz"; } || \
  fail "Failed to retrieve $VERSION"

rm "${VERSION}.tar.gz"
IDENT=$(echo * | sed 's/Isabelle-repository-//')

rm "Isabelle-repository-$IDENT/.hg_archival.txt"
rm "Isabelle-repository-$IDENT/.hgtags"


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

cd "$DISTBASE"
mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
rm -rf "$DISTPREFIX/$TMP"

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


# website

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
DISTBASE=$DISTBASE
EOF

cp lib/html/library_index_content.template ../website/


# prepare dist for release

echo "###"
echo "### Preparing distribution $DISTNAME"
echo "###"

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

./Admin/build all || fail "Failed to build distribution"
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/codegen_process.pdf
rm -rf doc-src

mkdir contrib

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/" src/Pure/ROOT.ML
fi

perl -pi -e "s/val changelog = \"\"/val changelog = \"$REPOS/log/$IDENT\"/" src/Pure/ROOT.ML
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


# create archives

echo "###"
echo "### Creating archives ..."
echo "###"

cd "$DISTBASE"

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

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 -c -z -f "$DISTNAME.tar.gz" Isabelle "$DISTNAME"

echo "${DISTNAME}_pdf.tar.gz"
tar -C pdf -c -z -f "${DISTNAME}_pdf.tar.gz" "$DISTNAME"

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