1.1 --- a/Admin/CHECKLIST Thu Jul 05 13:35:46 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,81 +0,0 @@
1.4 -Checklist for official releases
1.5 -===============================
1.6 -
1.7 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
1.8 -
1.9 -- test Proof General 4.1, 3.7.1.1;
1.10 -
1.11 -- check HTML header of library;
1.12 -
1.13 -- check CTRL-C, SIGINT in tty (also for external processes);
1.14 -
1.15 -- check persistent sessions with PG and Poly/ML 5.x;
1.16 -
1.17 -- check file positions within logic images (hyperlinks etc.);
1.18 -
1.19 -- Admin/update-keywords;
1.20 -
1.21 -- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
1.22 -
1.23 -- check Admin/contributed_components;
1.24 -
1.25 -- check funny base directory, e.g. "Test 中国";
1.26 -
1.27 -- diff NEWS wrt. last official release, which is read-only;
1.28 -
1.29 -- update https://isabelle.in.tum.de/repos/website;
1.30 -
1.31 -- maintain Docs:
1.32 - doc-src: make all
1.33 - doc-src/Dirs
1.34 - doc/Contents
1.35 -
1.36 -- maintain Logics:
1.37 - build
1.38 - etc/components
1.39 - lib/html/library_index_content.template
1.40 -
1.41 -- test separate compilation of Isabelle/Scala PIDE sources:
1.42 - Admin/build jars_test
1.43 -
1.44 -- test Isabelle/jEdit:
1.45 - print buffer
1.46 -
1.47 -- test contrib components:
1.48 - x86_64-linux without 32bit C/C++ libraries
1.49 - Mac OS X Leopard
1.50 -
1.51 -
1.52 -Packaging
1.53 -=========
1.54 -
1.55 -- makedist -j jedit_build-XXXX -r DISTNAME
1.56 -
1.57 -- makebin (multiplatform);
1.58 -
1.59 -- makebundle (multiplatform);
1.60 -
1.61 -- Mac OS X: hdiutil create -srcfolder DIR DMG;
1.62 -
1.63 -- Windows: cat 7zsd_All.sfx sfx.txt Isabelle.7z > Isabelle.exe
1.64 -
1.65 -- makebin -l on fast machine, based on renamed bundle with deleted heaps;
1.66 -
1.67 -
1.68 -Final release stage
1.69 -===================
1.70 -
1.71 -- makedist: REPOS_NAME="isabelle-release"
1.72 -
1.73 -- various .hg/hgrc files:
1.74 - default = /home/isabelle-repository/repos/isabelle-release
1.75 -
1.76 -- isatest@macbroy28:hg-isabelle/.hg/hgrc
1.77 -- isatest@macbroy28:devel-page/content/index.content
1.78 -
1.79 -
1.80 -Post-release
1.81 -============
1.82 -
1.83 -- update /home/isabelle and /home/isabelle/html-data
1.84 -
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/Admin/Release/CHECKLIST Thu Jul 05 14:13:14 2012 +0200
2.3 @@ -0,0 +1,81 @@
2.4 +Checklist for official releases
2.5 +===============================
2.6 +
2.7 +- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
2.8 +
2.9 +- test Proof General 4.1, 3.7.1.1;
2.10 +
2.11 +- check HTML header of library;
2.12 +
2.13 +- check CTRL-C, SIGINT in tty (also for external processes);
2.14 +
2.15 +- check persistent sessions with PG and Poly/ML 5.x;
2.16 +
2.17 +- check file positions within logic images (hyperlinks etc.);
2.18 +
2.19 +- Admin/update-keywords;
2.20 +
2.21 +- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
2.22 +
2.23 +- check Admin/components;
2.24 +
2.25 +- check funny base directory, e.g. "Test 中国";
2.26 +
2.27 +- diff NEWS wrt. last official release, which is read-only;
2.28 +
2.29 +- update https://isabelle.in.tum.de/repos/website;
2.30 +
2.31 +- maintain Docs:
2.32 + doc-src: make all
2.33 + doc-src/Dirs
2.34 + doc/Contents
2.35 +
2.36 +- maintain Logics:
2.37 + build
2.38 + etc/components
2.39 + lib/html/library_index_content.template
2.40 +
2.41 +- test separate compilation of Isabelle/Scala PIDE sources:
2.42 + Admin/build jars_test
2.43 +
2.44 +- test Isabelle/jEdit:
2.45 + print buffer
2.46 +
2.47 +- test contrib components:
2.48 + x86_64-linux without 32bit C/C++ libraries
2.49 + Mac OS X Leopard
2.50 +
2.51 +
2.52 +Packaging
2.53 +=========
2.54 +
2.55 +- makedist -j jedit_build-XXXX -r DISTNAME
2.56 +
2.57 +- makebin (multiplatform);
2.58 +
2.59 +- makebundle (multiplatform);
2.60 +
2.61 +- Mac OS X: hdiutil create -srcfolder DIR DMG;
2.62 +
2.63 +- Windows: cat 7zsd_All.sfx sfx.txt Isabelle.7z > Isabelle.exe
2.64 +
2.65 +- makebin -l on fast machine, based on renamed bundle with deleted heaps;
2.66 +
2.67 +
2.68 +Final release stage
2.69 +===================
2.70 +
2.71 +- makedist: REPOS_NAME="isabelle-release"
2.72 +
2.73 +- various .hg/hgrc files:
2.74 + default = /home/isabelle-repository/repos/isabelle-release
2.75 +
2.76 +- isatest@macbroy28:hg-isabelle/.hg/hgrc
2.77 +- isatest@macbroy28:devel-page/content/index.content
2.78 +
2.79 +
2.80 +Post-release
2.81 +============
2.82 +
2.83 +- update /home/isabelle and /home/isabelle/html-data
2.84 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/Admin/Release/isasync Thu Jul 05 14:13:14 2012 +0200
3.3 @@ -0,0 +1,129 @@
3.4 +#!/usr/bin/env bash
3.5 +#
3.6 +# mirror script for Isabelle distribution or website
3.7 +
3.8 +
3.9 +## diagnostics
3.10 +
3.11 +PRG=`basename "$0"`
3.12 +
3.13 +usage()
3.14 +{
3.15 + echo
3.16 + echo "Usage: $PRG [OPTIONS] DEST"
3.17 + echo
3.18 + echo " Options are:"
3.19 + echo " -h print help message"
3.20 + echo " -n dry run, don't do anything, just report what would happen"
3.21 + echo " -w (ignored for backward compatibility)"
3.22 + echo " -d delete files that are not on the server (BEWARE!)"
3.23 + echo
3.24 + exit 1
3.25 +}
3.26 +
3.27 +fail()
3.28 +{
3.29 + echo "$1" >&2
3.30 + exit 2
3.31 +}
3.32 +
3.33 +
3.34 +## process command line
3.35 +
3.36 +# options
3.37 +
3.38 +HELP=""
3.39 +ARGS=""
3.40 +SRC="isabelle-website"
3.41 +
3.42 +while getopts "hnwd" OPT
3.43 +do
3.44 + case "$OPT" in
3.45 + h)
3.46 + HELP=true
3.47 + ;;
3.48 + n)
3.49 + ARGS="$ARGS -n"
3.50 + ;;
3.51 + w)
3.52 + echo "option -w ignored"
3.53 + ;;
3.54 + d)
3.55 + ARGS="$ARGS --delete"
3.56 + ;;
3.57 + \?)
3.58 + usage
3.59 + ;;
3.60 + esac
3.61 +done
3.62 +
3.63 +shift `expr $OPTIND - 1`
3.64 +
3.65 +
3.66 +# help
3.67 +
3.68 +if [ -n "$HELP" ]; then
3.69 + cat <<EOF
3.70 +
3.71 +Mirroring the Isabelle distribution or website
3.72 +==============================================
3.73 +
3.74 +The Munich site maintains an rsync server for the Isabelle
3.75 +distribution or website.
3.76 +
3.77 +The rsync tool is very smart and efficient in mirroring large
3.78 +directory hierarchies. See http://rsync.samba.org/ for more
3.79 +information. The $PRG script provides a simple front-end
3.80 +for easy access to the Isabelle distribution.
3.81 +
3.82 +The script can be either run in conservative or clean-sweep mode.
3.83 +
3.84 +1) Basic mirroring works like this:
3.85 +
3.86 + $PRG /foo/bar
3.87 +
3.88 +where /foo/bar refers to your local copy of the Isabelle distribution
3.89 +(the base directory has to exist already). This operation is
3.90 +conservative in the sense that files are never deleted, thus garbage
3.91 +may accumulate over time as our master copy is changed.
3.92 +
3.93 +Avoiding garbage in your local copy requires some care. Rsync
3.94 +provides a way to delete all additional local files that are absent in
3.95 +the master copy. This provides an efficient way to purge large
3.96 +directory hierarchies, even unwillingly in case that a wrong
3.97 +destination is given!
3.98 +
3.99 +2a) This will invoke a safe dry-run of clean-sweep mirroring:
3.100 +
3.101 + $PRG -dn /foo/bar
3.102 +
3.103 +where additions and deletions will be printed without any actual
3.104 +changes performed so far.
3.105 +
3.106 +2b) Exact mirroring with actual deletion of garbage may be performed
3.107 +like this:
3.108 +
3.109 + $PRG -d /foo/bar
3.110 +
3.111 +
3.112 +After gaining some confidence in the workings of $PRG one
3.113 +would usually set up some automatic mirror scheme, e.g. a daily cron
3.114 +job run by the 'nobody' user.
3.115 +
3.116 +Add -w to the option list in order to mirror the whole Isabelle website
3.117 +
3.118 +EOF
3.119 + exit 0
3.120 +fi
3.121 +
3.122 +
3.123 +# arguments
3.124 +
3.125 +[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
3.126 +
3.127 +DEST="$1"; shift;
3.128 +
3.129 +
3.130 +## main
3.131 +
3.132 +exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/Admin/Release/makebin Thu Jul 05 14:13:14 2012 +0200
4.3 @@ -0,0 +1,118 @@
4.4 +#!/usr/bin/env bash
4.5 +#
4.6 +# makebin -- make Isabelle logic images for current platform
4.7 +
4.8 +
4.9 +## global settings
4.10 +
4.11 +TMP="/var/tmp/isabelle-makebin$$"
4.12 +
4.13 +
4.14 +## diagnostics
4.15 +
4.16 +PRG=$(basename "$0")
4.17 +
4.18 +function usage()
4.19 +{
4.20 + echo
4.21 + echo "Usage: $PRG [OPTIONS] ARCHIVE"
4.22 + echo
4.23 + echo " Options are:"
4.24 + echo " -l produce library"
4.25 + echo
4.26 + echo " Precompile Isabelle for the current platform."
4.27 + echo
4.28 + exit 1
4.29 +}
4.30 +
4.31 +function fail()
4.32 +{
4.33 + echo "$1" >&2
4.34 + exit 2
4.35 +}
4.36 +
4.37 +
4.38 +## process command line
4.39 +
4.40 +# options
4.41 +
4.42 +DO_LIBRARY=""
4.43 +
4.44 +while getopts "l" OPT
4.45 +do
4.46 + case "$OPT" in
4.47 + l)
4.48 + DO_LIBRARY=true
4.49 + ;;
4.50 + \?)
4.51 + usage
4.52 + ;;
4.53 + esac
4.54 +done
4.55 +
4.56 +shift $(($OPTIND - 1))
4.57 +
4.58 +
4.59 +# args
4.60 +
4.61 +[ "$#" -gt 1 ] && usage
4.62 +
4.63 +ARCHIVE="$1"; shift
4.64 +
4.65 +
4.66 +## main
4.67 +
4.68 +[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
4.69 +ARCHIVE_BASE="$(basename "$ARCHIVE")"
4.70 +ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
4.71 +ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
4.72 +
4.73 +ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
4.74 +ISABELLE_HOME="$TMP/$ISABELLE_NAME"
4.75 +
4.76 +
4.77 +# build logics
4.78 +
4.79 +mkdir "$TMP" || fail "Cannot create directory $TMP"
4.80 +
4.81 +cd "$TMP"
4.82 +tar xzf "$ARCHIVE_FULL"
4.83 +cd "$ISABELLE_NAME"
4.84 +
4.85 +perl -pi \
4.86 + -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
4.87 + etc/settings
4.88 +
4.89 +if [ -n "$DO_LIBRARY" ]; then
4.90 + perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
4.91 + etc/settings
4.92 +fi
4.93 +
4.94 +ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
4.95 +
4.96 +COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
4.97 +PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
4.98 +
4.99 +if [ -n "$DO_LIBRARY" ]; then
4.100 + ./build -bait -m all
4.101 +else
4.102 + ./build -b HOL
4.103 +fi
4.104 +
4.105 +
4.106 +# prepare result
4.107 +
4.108 +cd "$TMP"
4.109 +
4.110 +chmod -R g=o "$TMP"
4.111 +chgrp -R isabelle "$TMP"
4.112 +
4.113 +if [ -n "$DO_LIBRARY" ]; then
4.114 + tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
4.115 +else
4.116 + tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
4.117 +fi
4.118 +
4.119 +
4.120 +# clean up
4.121 +rm -rf "$TMP"
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/Admin/Release/makebundle Thu Jul 05 14:13:14 2012 +0200
5.3 @@ -0,0 +1,147 @@
5.4 +#!/usr/bin/env bash
5.5 +#
5.6 +# makebundle -- re-package with add-on components
5.7 +
5.8 +## diagnostics
5.9 +
5.10 +PRG=$(basename "$0")
5.11 +
5.12 +function usage()
5.13 +{
5.14 + echo
5.15 + echo "Usage: $PRG ARCHIVE PLATFORM"
5.16 + echo
5.17 + echo " Re-package Isabelle source distribution with add-on components"
5.18 + echo " and heap images"
5.19 + echo
5.20 + exit 1
5.21 +}
5.22 +
5.23 +function fail()
5.24 +{
5.25 + echo "$1" >&2
5.26 + exit 2
5.27 +}
5.28 +
5.29 +
5.30 +## implicit and explicit arguments
5.31 +
5.32 +TMP="/var/tmp/isabelle-makebundle$$"
5.33 +mkdir "$TMP" || fail "Cannot create directory $TMP"
5.34 +
5.35 +[ "$#" -ne 2 ] && usage
5.36 +
5.37 +ARCHIVE="$1"; shift
5.38 +PLATFORM="$1"; shift
5.39 +
5.40 +[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
5.41 +
5.42 +
5.43 +## main
5.44 +
5.45 +ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
5.46 +ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
5.47 +ISABELLE_HOME="$TMP/$ISABELLE_NAME"
5.48 +
5.49 +tar -C "$TMP" -x -z -f "$ARCHIVE"
5.50 +
5.51 +
5.52 +echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
5.53 +
5.54 +for CONTRIB in "$ARCHIVE_DIR/contrib/"*.tar.gz "$ARCHIVE_DIR/contrib/$PLATFORM"/*.tar.gz
5.55 +do
5.56 + if [ -f "$CONTRIB" ]; then
5.57 + tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
5.58 + NAME="$(basename "$CONTRIB" .tar.gz)"
5.59 + [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
5.60 +
5.61 + if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
5.62 + echo "component $NAME"
5.63 + if [ "$PLATFORM" != x86-cygwin -a "$NAME" = ProofGeneral-3.7.1.1 ]; then
5.64 + echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
5.65 + elif [ "$PLATFORM" = x86-cygwin -a "$NAME" = ProofGeneral-4.1 ]; then
5.66 + echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
5.67 + else
5.68 + echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
5.69 + fi
5.70 + else
5.71 + echo "package $NAME"
5.72 + fi
5.73 + fi
5.74 +done
5.75 +
5.76 +if [ "$PLATFORM" = x86-cygwin ]; then
5.77 + TAR="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.tar"
5.78 + [ -e "$TAR" ] || fail "Missing $TAR"
5.79 + rm -f "$ISABELLE_HOME/Isabelle"
5.80 + tar -C "$ISABELLE_HOME" -xv -f "$TAR"
5.81 +
5.82 + (
5.83 + cd "$ISABELLE_HOME"
5.84 + for DIR in $(find contrib -name x86-linux -o -name x86_64-linux -o -name x86-darwin -o -name x86_64-darwin | sort)
5.85 + do
5.86 + echo "removing $DIR"
5.87 + rm -rf "$DIR"
5.88 + done
5.89 + )
5.90 +
5.91 + mv "$ISABELLE_HOME/contrib"/polyml* "$ISABELLE_HOME/contrib/cygwin-1.7.9/usr/local/"
5.92 + (
5.93 + cd "$ISABELLE_HOME/contrib/cygwin-1.7.9"
5.94 + find usr/local/polyml-*/x86-cygwin | gzip > etc/setup/polyml.lst.gz
5.95 + )
5.96 +
5.97 + for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
5.98 + do
5.99 + FILE="$ISABELLE_HOME/$NAME"
5.100 + {
5.101 + echo '<?xml version="1.0" encoding="utf-8" ?>'
5.102 + echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
5.103 + echo '<html xmlns="http://www.w3.org/1999/xhtml">'
5.104 + echo '<head>'
5.105 + echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
5.106 + echo "<title>${NAME}</title>"
5.107 + echo '</head>'
5.108 + echo '<body>'
5.109 + echo '<pre>'
5.110 + perl -w -p -e "s/&/&/g; s/</</g; s/>/>/g; s/'/'/g; s/\"/"/g;" "$FILE"
5.111 + echo '</pre>'
5.112 + echo '</body>'
5.113 + } > "${FILE}.html"
5.114 + done
5.115 +fi
5.116 +
5.117 +
5.118 +HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
5.119 +[ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
5.120 +echo "heaps"
5.121 +tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
5.122 +
5.123 +case "$PLATFORM" in
5.124 + x86_64-linux)
5.125 + perl -pi -e 's,^ML_PLATFORM=.*$,ML_PLATFORM="\$ISABELLE_PLATFORM64",g;' "$TMP/$ISABELLE_NAME/etc/settings"
5.126 + perl -pi -e "s,^ML_OPTIONS=.*$,ML_OPTIONS=\"-H 400\",g;" "$TMP/$ISABELLE_NAME/etc/settings"
5.127 + ;;
5.128 + *-darwin)
5.129 + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
5.130 + -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
5.131 + -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
5.132 + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
5.133 + ;;
5.134 + *-cygwin)
5.135 + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
5.136 + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
5.137 + ;;
5.138 + *)
5.139 + ;;
5.140 +esac
5.141 +
5.142 +BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
5.143 +
5.144 +echo "$(basename "$BUNDLE_ARCHIVE")"
5.145 +tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
5.146 +
5.147 +
5.148 +# clean up
5.149 +cd /tmp
5.150 +rm -rf "$TMP"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/Admin/Release/makedist Thu Jul 05 14:13:14 2012 +0200
6.3 @@ -0,0 +1,235 @@
6.4 +#!/usr/bin/env bash
6.5 +#
6.6 +# makedist -- make Isabelle source distribution
6.7 +
6.8 +## global settings
6.9 +
6.10 +REPOS_NAME="isabelle"
6.11 +REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
6.12 +DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
6.13 +
6.14 +umask 022
6.15 +
6.16 +
6.17 +## diagnostics
6.18 +
6.19 +PRG="$(basename "$0")"
6.20 +THIS="$(cd $(dirname "$0"); pwd)"
6.21 +
6.22 +function usage()
6.23 +{
6.24 + cat <<EOF
6.25 +
6.26 +Usage: $PRG [OPTIONS] [VERSION]
6.27 +
6.28 + Options are:
6.29 + -j JEDIT_BUILD build Isabelle/jEdit via given jedit_build component
6.30 + -r RELEASE proper release with name"
6.31 +
6.32 + Make Isabelle distribution from the main Mercurial repository at TUM.
6.33 +
6.34 + VERSION identifies the snapshot, using usual Mercurial terminology;
6.35 + the default is RELEASE if given, otherwise "tip".
6.36 +
6.37 +EOF
6.38 + exit 1
6.39 +}
6.40 +
6.41 +function fail()
6.42 +{
6.43 + echo "$1" >&2
6.44 + exit 2
6.45 +}
6.46 +
6.47 +
6.48 +## process command line
6.49 +
6.50 +# options
6.51 +
6.52 +RELEASE=""
6.53 +ISABELLE_JEDIT_BUILD_HOME=""
6.54 +
6.55 +while getopts "j:r:" OPT
6.56 +do
6.57 + case "$OPT" in
6.58 + j)
6.59 + ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
6.60 + ;;
6.61 + r)
6.62 + RELEASE="$OPTARG"
6.63 + ;;
6.64 + \?)
6.65 + usage
6.66 + ;;
6.67 + esac
6.68 +done
6.69 +
6.70 +shift $(($OPTIND - 1))
6.71 +
6.72 +
6.73 +# args
6.74 +
6.75 +VERSION=""
6.76 +[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
6.77 +[ -z "$VERSION" ] && VERSION="$RELEASE"
6.78 +[ -z "$VERSION" ] && VERSION="tip"
6.79 +
6.80 +[ "$#" -gt 0 ] && usage
6.81 +
6.82 +
6.83 +## main
6.84 +
6.85 +# tmp
6.86 +
6.87 +TMP="tmp-$USER$$"
6.88 +function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
6.89 +
6.90 +
6.91 +# retrieve archive and resolve version identifier
6.92 +
6.93 +mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
6.94 +cd "$DISTPREFIX/$TMP"
6.95 +
6.96 +echo "###"
6.97 +echo "### Retrieving Mercurial repository $VERSION"
6.98 +echo "###"
6.99 +
6.100 +if expr match "$REPOS" "https\?://" > /dev/null
6.101 +then
6.102 + { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
6.103 + fail "Failed to retrieve $VERSION"
6.104 +else
6.105 + { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
6.106 + fail "Failed to retrieve $VERSION"
6.107 +fi
6.108 +
6.109 +IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
6.110 +
6.111 +rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
6.112 +rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
6.113 +rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
6.114 +rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
6.115 +
6.116 +
6.117 +# dist name
6.118 +
6.119 +DATE=$(env LC_ALL=C date "+%d-%b-%Y")
6.120 +DISTDATE=$(env LC_ALL=C date "+%B %Y")
6.121 +
6.122 +if [ -z "$RELEASE" ]; then
6.123 + DISTNAME="Isabelle_$DATE"
6.124 + DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
6.125 +else
6.126 + DISTNAME="$RELEASE"
6.127 + DISTVERSION="$DISTNAME: $DISTDATE"
6.128 +fi
6.129 +
6.130 +DISTBASE="$DISTPREFIX/dist-$DISTNAME"
6.131 +mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
6.132 +[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
6.133 +
6.134 +cd "$DISTBASE"
6.135 +mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
6.136 +purge_tmp
6.137 +
6.138 +cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
6.139 +
6.140 +
6.141 +# prepare dist for release
6.142 +
6.143 +echo "###"
6.144 +echo "### Preparing distribution $DISTNAME"
6.145 +echo "###"
6.146 +
6.147 +rm -f .hgignore
6.148 +find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
6.149 +find . -print | xargs chmod -f u+rw
6.150 +
6.151 +perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
6.152 +
6.153 +./Admin/build all || fail "Failed to build distribution"
6.154 +
6.155 +if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
6.156 + [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""
6.157 + eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"
6.158 + [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"
6.159 + export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION
6.160 + ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
6.161 +fi
6.162 +
6.163 +rm -rf Admin
6.164 +
6.165 +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')
6.166 +mv -f $MOVE doc
6.167 +rm doc/Isa-logics.eps
6.168 +rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
6.169 +rm -rf doc-src
6.170 +
6.171 +mkdir -p contrib
6.172 +cat >contrib/README <<EOF
6.173 +This directory contains add-on components that contribute to the main
6.174 +Isabelle distribution. Separate licensing conditions apply, see each
6.175 +directory individually.
6.176 +EOF
6.177 +
6.178 +cp doc/isabelle*.eps lib/logo
6.179 +
6.180 +if [ -z "$RELEASE" ]; then
6.181 + {
6.182 + echo
6.183 + echo "IMPORTANT NOTE"
6.184 + echo "=============="
6.185 + echo
6.186 + echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
6.187 + echo "See $REPOS/log/$IDENT for details."
6.188 + echo
6.189 + } >ANNOUNCE
6.190 +else
6.191 + perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
6.192 +fi
6.193 +
6.194 +perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
6.195 +perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
6.196 +perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
6.197 +perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
6.198 +perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
6.199 +perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
6.200 +
6.201 +
6.202 +# create archive
6.203 +
6.204 +echo "###"
6.205 +echo "### Creating archive ..."
6.206 +echo "###"
6.207 +
6.208 +cd "$DISTBASE"
6.209 +
6.210 +echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
6.211 +echo "$IDENT" >../ISABELLE_IDENT
6.212 +
6.213 +chown -R "$LOGNAME" "$DISTNAME"
6.214 +chmod -R u+w "$DISTNAME"
6.215 +chmod -R g=o "$DISTNAME"
6.216 +chgrp -R isabelle "$DISTNAME"
6.217 +
6.218 +echo "$DISTNAME.tar.gz"
6.219 +tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
6.220 +
6.221 +
6.222 +# cleanup dist
6.223 +
6.224 +mv "$DISTNAME" "${DISTNAME}-old"
6.225 +mkdir "$DISTNAME"
6.226 +
6.227 +mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
6.228 + "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
6.229 +mkdir "$DISTNAME/doc"
6.230 +mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
6.231 +
6.232 +rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
6.233 +
6.234 +chgrp -R isabelle "$DISTNAME"
6.235 +
6.236 +rm -rf "${DISTNAME}-old"
6.237 +
6.238 +echo "DONE"
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/Admin/Release/mirror-website Thu Jul 05 14:13:14 2012 +0200
7.3 @@ -0,0 +1,21 @@
7.4 +#!/usr/bin/env bash
7.5 +#
7.6 +# mirrors the Isabelle website
7.7 +
7.8 +HOST=$(hostname)
7.9 +
7.10 +case ${HOST} in
7.11 + sunbroy* | atbroy* | macbroy*)
7.12 + DEST=/home/html/isabelle/html-data
7.13 + ;;
7.14 + *.cl.cam.ac.uk)
7.15 + USER=paulson
7.16 + DEST=/anfs/www/html/research/hvg/Isabelle
7.17 + ;;
7.18 + *)
7.19 + echo "Unknown destination directory for ${HOST}"
7.20 + exit 2
7.21 + ;;
7.22 +esac
7.23 +
7.24 +exec $(dirname $0)/isasync $DEST
8.1 --- a/Admin/isasync Thu Jul 05 13:35:46 2012 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,129 +0,0 @@
8.4 -#!/usr/bin/env bash
8.5 -#
8.6 -# mirror script for Isabelle distribution or website
8.7 -
8.8 -
8.9 -## diagnostics
8.10 -
8.11 -PRG=`basename "$0"`
8.12 -
8.13 -usage()
8.14 -{
8.15 - echo
8.16 - echo "Usage: $PRG [OPTIONS] DEST"
8.17 - echo
8.18 - echo " Options are:"
8.19 - echo " -h print help message"
8.20 - echo " -n dry run, don't do anything, just report what would happen"
8.21 - echo " -w (ignored for backward compatibility)"
8.22 - echo " -d delete files that are not on the server (BEWARE!)"
8.23 - echo
8.24 - exit 1
8.25 -}
8.26 -
8.27 -fail()
8.28 -{
8.29 - echo "$1" >&2
8.30 - exit 2
8.31 -}
8.32 -
8.33 -
8.34 -## process command line
8.35 -
8.36 -# options
8.37 -
8.38 -HELP=""
8.39 -ARGS=""
8.40 -SRC="isabelle-website"
8.41 -
8.42 -while getopts "hnwd" OPT
8.43 -do
8.44 - case "$OPT" in
8.45 - h)
8.46 - HELP=true
8.47 - ;;
8.48 - n)
8.49 - ARGS="$ARGS -n"
8.50 - ;;
8.51 - w)
8.52 - echo "option -w ignored"
8.53 - ;;
8.54 - d)
8.55 - ARGS="$ARGS --delete"
8.56 - ;;
8.57 - \?)
8.58 - usage
8.59 - ;;
8.60 - esac
8.61 -done
8.62 -
8.63 -shift `expr $OPTIND - 1`
8.64 -
8.65 -
8.66 -# help
8.67 -
8.68 -if [ -n "$HELP" ]; then
8.69 - cat <<EOF
8.70 -
8.71 -Mirroring the Isabelle distribution or website
8.72 -==============================================
8.73 -
8.74 -The Munich site maintains an rsync server for the Isabelle
8.75 -distribution or website.
8.76 -
8.77 -The rsync tool is very smart and efficient in mirroring large
8.78 -directory hierarchies. See http://rsync.samba.org/ for more
8.79 -information. The $PRG script provides a simple front-end
8.80 -for easy access to the Isabelle distribution.
8.81 -
8.82 -The script can be either run in conservative or clean-sweep mode.
8.83 -
8.84 -1) Basic mirroring works like this:
8.85 -
8.86 - $PRG /foo/bar
8.87 -
8.88 -where /foo/bar refers to your local copy of the Isabelle distribution
8.89 -(the base directory has to exist already). This operation is
8.90 -conservative in the sense that files are never deleted, thus garbage
8.91 -may accumulate over time as our master copy is changed.
8.92 -
8.93 -Avoiding garbage in your local copy requires some care. Rsync
8.94 -provides a way to delete all additional local files that are absent in
8.95 -the master copy. This provides an efficient way to purge large
8.96 -directory hierarchies, even unwillingly in case that a wrong
8.97 -destination is given!
8.98 -
8.99 -2a) This will invoke a safe dry-run of clean-sweep mirroring:
8.100 -
8.101 - $PRG -dn /foo/bar
8.102 -
8.103 -where additions and deletions will be printed without any actual
8.104 -changes performed so far.
8.105 -
8.106 -2b) Exact mirroring with actual deletion of garbage may be performed
8.107 -like this:
8.108 -
8.109 - $PRG -d /foo/bar
8.110 -
8.111 -
8.112 -After gaining some confidence in the workings of $PRG one
8.113 -would usually set up some automatic mirror scheme, e.g. a daily cron
8.114 -job run by the 'nobody' user.
8.115 -
8.116 -Add -w to the option list in order to mirror the whole Isabelle website
8.117 -
8.118 -EOF
8.119 - exit 0
8.120 -fi
8.121 -
8.122 -
8.123 -# arguments
8.124 -
8.125 -[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
8.126 -
8.127 -DEST="$1"; shift;
8.128 -
8.129 -
8.130 -## main
8.131 -
8.132 -exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"
9.1 --- a/Admin/makebin Thu Jul 05 13:35:46 2012 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,118 +0,0 @@
9.4 -#!/usr/bin/env bash
9.5 -#
9.6 -# makebin -- make Isabelle logic images for current platform
9.7 -
9.8 -
9.9 -## global settings
9.10 -
9.11 -TMP="/var/tmp/isabelle-makebin$$"
9.12 -
9.13 -
9.14 -## diagnostics
9.15 -
9.16 -PRG=$(basename "$0")
9.17 -
9.18 -function usage()
9.19 -{
9.20 - echo
9.21 - echo "Usage: $PRG [OPTIONS] ARCHIVE"
9.22 - echo
9.23 - echo " Options are:"
9.24 - echo " -l produce library"
9.25 - echo
9.26 - echo " Precompile Isabelle for the current platform."
9.27 - echo
9.28 - exit 1
9.29 -}
9.30 -
9.31 -function fail()
9.32 -{
9.33 - echo "$1" >&2
9.34 - exit 2
9.35 -}
9.36 -
9.37 -
9.38 -## process command line
9.39 -
9.40 -# options
9.41 -
9.42 -DO_LIBRARY=""
9.43 -
9.44 -while getopts "l" OPT
9.45 -do
9.46 - case "$OPT" in
9.47 - l)
9.48 - DO_LIBRARY=true
9.49 - ;;
9.50 - \?)
9.51 - usage
9.52 - ;;
9.53 - esac
9.54 -done
9.55 -
9.56 -shift $(($OPTIND - 1))
9.57 -
9.58 -
9.59 -# args
9.60 -
9.61 -[ "$#" -gt 1 ] && usage
9.62 -
9.63 -ARCHIVE="$1"; shift
9.64 -
9.65 -
9.66 -## main
9.67 -
9.68 -[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
9.69 -ARCHIVE_BASE="$(basename "$ARCHIVE")"
9.70 -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
9.71 -ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
9.72 -
9.73 -ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
9.74 -ISABELLE_HOME="$TMP/$ISABELLE_NAME"
9.75 -
9.76 -
9.77 -# build logics
9.78 -
9.79 -mkdir "$TMP" || fail "Cannot create directory $TMP"
9.80 -
9.81 -cd "$TMP"
9.82 -tar xzf "$ARCHIVE_FULL"
9.83 -cd "$ISABELLE_NAME"
9.84 -
9.85 -perl -pi \
9.86 - -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
9.87 - etc/settings
9.88 -
9.89 -if [ -n "$DO_LIBRARY" ]; then
9.90 - perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
9.91 - etc/settings
9.92 -fi
9.93 -
9.94 -ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
9.95 -
9.96 -COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
9.97 -PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
9.98 -
9.99 -if [ -n "$DO_LIBRARY" ]; then
9.100 - ./build -bait -m all
9.101 -else
9.102 - ./build -b HOL
9.103 -fi
9.104 -
9.105 -
9.106 -# prepare result
9.107 -
9.108 -cd "$TMP"
9.109 -
9.110 -chmod -R g=o "$TMP"
9.111 -chgrp -R isabelle "$TMP"
9.112 -
9.113 -if [ -n "$DO_LIBRARY" ]; then
9.114 - tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
9.115 -else
9.116 - tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
9.117 -fi
9.118 -
9.119 -
9.120 -# clean up
9.121 -rm -rf "$TMP"
10.1 --- a/Admin/makebundle Thu Jul 05 13:35:46 2012 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,147 +0,0 @@
10.4 -#!/usr/bin/env bash
10.5 -#
10.6 -# makebundle -- re-package with add-on components
10.7 -
10.8 -## diagnostics
10.9 -
10.10 -PRG=$(basename "$0")
10.11 -
10.12 -function usage()
10.13 -{
10.14 - echo
10.15 - echo "Usage: $PRG ARCHIVE PLATFORM"
10.16 - echo
10.17 - echo " Re-package Isabelle source distribution with add-on components"
10.18 - echo " and heap images"
10.19 - echo
10.20 - exit 1
10.21 -}
10.22 -
10.23 -function fail()
10.24 -{
10.25 - echo "$1" >&2
10.26 - exit 2
10.27 -}
10.28 -
10.29 -
10.30 -## implicit and explicit arguments
10.31 -
10.32 -TMP="/var/tmp/isabelle-makebundle$$"
10.33 -mkdir "$TMP" || fail "Cannot create directory $TMP"
10.34 -
10.35 -[ "$#" -ne 2 ] && usage
10.36 -
10.37 -ARCHIVE="$1"; shift
10.38 -PLATFORM="$1"; shift
10.39 -
10.40 -[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
10.41 -
10.42 -
10.43 -## main
10.44 -
10.45 -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
10.46 -ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
10.47 -ISABELLE_HOME="$TMP/$ISABELLE_NAME"
10.48 -
10.49 -tar -C "$TMP" -x -z -f "$ARCHIVE"
10.50 -
10.51 -
10.52 -echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
10.53 -
10.54 -for CONTRIB in "$ARCHIVE_DIR/contrib/"*.tar.gz "$ARCHIVE_DIR/contrib/$PLATFORM"/*.tar.gz
10.55 -do
10.56 - if [ -f "$CONTRIB" ]; then
10.57 - tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
10.58 - NAME="$(basename "$CONTRIB" .tar.gz)"
10.59 - [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
10.60 -
10.61 - if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
10.62 - echo "component $NAME"
10.63 - if [ "$PLATFORM" != x86-cygwin -a "$NAME" = ProofGeneral-3.7.1.1 ]; then
10.64 - echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
10.65 - elif [ "$PLATFORM" = x86-cygwin -a "$NAME" = ProofGeneral-4.1 ]; then
10.66 - echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
10.67 - else
10.68 - echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
10.69 - fi
10.70 - else
10.71 - echo "package $NAME"
10.72 - fi
10.73 - fi
10.74 -done
10.75 -
10.76 -if [ "$PLATFORM" = x86-cygwin ]; then
10.77 - TAR="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.tar"
10.78 - [ -e "$TAR" ] || fail "Missing $TAR"
10.79 - rm -f "$ISABELLE_HOME/Isabelle"
10.80 - tar -C "$ISABELLE_HOME" -xv -f "$TAR"
10.81 -
10.82 - (
10.83 - cd "$ISABELLE_HOME"
10.84 - for DIR in $(find contrib -name x86-linux -o -name x86_64-linux -o -name x86-darwin -o -name x86_64-darwin | sort)
10.85 - do
10.86 - echo "removing $DIR"
10.87 - rm -rf "$DIR"
10.88 - done
10.89 - )
10.90 -
10.91 - mv "$ISABELLE_HOME/contrib"/polyml* "$ISABELLE_HOME/contrib/cygwin-1.7.9/usr/local/"
10.92 - (
10.93 - cd "$ISABELLE_HOME/contrib/cygwin-1.7.9"
10.94 - find usr/local/polyml-*/x86-cygwin | gzip > etc/setup/polyml.lst.gz
10.95 - )
10.96 -
10.97 - for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
10.98 - do
10.99 - FILE="$ISABELLE_HOME/$NAME"
10.100 - {
10.101 - echo '<?xml version="1.0" encoding="utf-8" ?>'
10.102 - echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
10.103 - echo '<html xmlns="http://www.w3.org/1999/xhtml">'
10.104 - echo '<head>'
10.105 - echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
10.106 - echo "<title>${NAME}</title>"
10.107 - echo '</head>'
10.108 - echo '<body>'
10.109 - echo '<pre>'
10.110 - perl -w -p -e "s/&/&/g; s/</</g; s/>/>/g; s/'/'/g; s/\"/"/g;" "$FILE"
10.111 - echo '</pre>'
10.112 - echo '</body>'
10.113 - } > "${FILE}.html"
10.114 - done
10.115 -fi
10.116 -
10.117 -
10.118 -HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
10.119 -[ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
10.120 -echo "heaps"
10.121 -tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
10.122 -
10.123 -case "$PLATFORM" in
10.124 - x86_64-linux)
10.125 - perl -pi -e 's,^ML_PLATFORM=.*$,ML_PLATFORM="\$ISABELLE_PLATFORM64",g;' "$TMP/$ISABELLE_NAME/etc/settings"
10.126 - perl -pi -e "s,^ML_OPTIONS=.*$,ML_OPTIONS=\"-H 400\",g;" "$TMP/$ISABELLE_NAME/etc/settings"
10.127 - ;;
10.128 - *-darwin)
10.129 - perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
10.130 - -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
10.131 - -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
10.132 - "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
10.133 - ;;
10.134 - *-cygwin)
10.135 - perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
10.136 - "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
10.137 - ;;
10.138 - *)
10.139 - ;;
10.140 -esac
10.141 -
10.142 -BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
10.143 -
10.144 -echo "$(basename "$BUNDLE_ARCHIVE")"
10.145 -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
10.146 -
10.147 -
10.148 -# clean up
10.149 -cd /tmp
10.150 -rm -rf "$TMP"
11.1 --- a/Admin/makedist Thu Jul 05 13:35:46 2012 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,235 +0,0 @@
11.4 -#!/usr/bin/env bash
11.5 -#
11.6 -# makedist -- make Isabelle source distribution
11.7 -
11.8 -## global settings
11.9 -
11.10 -REPOS_NAME="isabelle"
11.11 -REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
11.12 -DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
11.13 -
11.14 -umask 022
11.15 -
11.16 -
11.17 -## diagnostics
11.18 -
11.19 -PRG="$(basename "$0")"
11.20 -THIS="$(cd $(dirname "$0"); pwd)"
11.21 -
11.22 -function usage()
11.23 -{
11.24 - cat <<EOF
11.25 -
11.26 -Usage: $PRG [OPTIONS] [VERSION]
11.27 -
11.28 - Options are:
11.29 - -j JEDIT_BUILD build Isabelle/jEdit via given jedit_build component
11.30 - -r RELEASE proper release with name"
11.31 -
11.32 - Make Isabelle distribution from the main Mercurial repository at TUM.
11.33 -
11.34 - VERSION identifies the snapshot, using usual Mercurial terminology;
11.35 - the default is RELEASE if given, otherwise "tip".
11.36 -
11.37 -EOF
11.38 - exit 1
11.39 -}
11.40 -
11.41 -function fail()
11.42 -{
11.43 - echo "$1" >&2
11.44 - exit 2
11.45 -}
11.46 -
11.47 -
11.48 -## process command line
11.49 -
11.50 -# options
11.51 -
11.52 -RELEASE=""
11.53 -ISABELLE_JEDIT_BUILD_HOME=""
11.54 -
11.55 -while getopts "j:r:" OPT
11.56 -do
11.57 - case "$OPT" in
11.58 - j)
11.59 - ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
11.60 - ;;
11.61 - r)
11.62 - RELEASE="$OPTARG"
11.63 - ;;
11.64 - \?)
11.65 - usage
11.66 - ;;
11.67 - esac
11.68 -done
11.69 -
11.70 -shift $(($OPTIND - 1))
11.71 -
11.72 -
11.73 -# args
11.74 -
11.75 -VERSION=""
11.76 -[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
11.77 -[ -z "$VERSION" ] && VERSION="$RELEASE"
11.78 -[ -z "$VERSION" ] && VERSION="tip"
11.79 -
11.80 -[ "$#" -gt 0 ] && usage
11.81 -
11.82 -
11.83 -## main
11.84 -
11.85 -# tmp
11.86 -
11.87 -TMP="tmp-$USER$$"
11.88 -function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
11.89 -
11.90 -
11.91 -# retrieve archive and resolve version identifier
11.92 -
11.93 -mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
11.94 -cd "$DISTPREFIX/$TMP"
11.95 -
11.96 -echo "###"
11.97 -echo "### Retrieving Mercurial repository $VERSION"
11.98 -echo "###"
11.99 -
11.100 -if expr match "$REPOS" "https\?://" > /dev/null
11.101 -then
11.102 - { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
11.103 - fail "Failed to retrieve $VERSION"
11.104 -else
11.105 - { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
11.106 - fail "Failed to retrieve $VERSION"
11.107 -fi
11.108 -
11.109 -IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
11.110 -
11.111 -rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
11.112 -rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
11.113 -rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
11.114 -rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
11.115 -
11.116 -
11.117 -# dist name
11.118 -
11.119 -DATE=$(env LC_ALL=C date "+%d-%b-%Y")
11.120 -DISTDATE=$(env LC_ALL=C date "+%B %Y")
11.121 -
11.122 -if [ -z "$RELEASE" ]; then
11.123 - DISTNAME="Isabelle_$DATE"
11.124 - DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
11.125 -else
11.126 - DISTNAME="$RELEASE"
11.127 - DISTVERSION="$DISTNAME: $DISTDATE"
11.128 -fi
11.129 -
11.130 -DISTBASE="$DISTPREFIX/dist-$DISTNAME"
11.131 -mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
11.132 -[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
11.133 -
11.134 -cd "$DISTBASE"
11.135 -mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
11.136 -purge_tmp
11.137 -
11.138 -cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
11.139 -
11.140 -
11.141 -# prepare dist for release
11.142 -
11.143 -echo "###"
11.144 -echo "### Preparing distribution $DISTNAME"
11.145 -echo "###"
11.146 -
11.147 -rm -f .hgignore
11.148 -find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
11.149 -find . -print | xargs chmod -f u+rw
11.150 -
11.151 -perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
11.152 -
11.153 -./Admin/build all || fail "Failed to build distribution"
11.154 -
11.155 -if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
11.156 - [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""
11.157 - eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"
11.158 - [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"
11.159 - export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION
11.160 - ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
11.161 -fi
11.162 -
11.163 -rm -rf Admin
11.164 -
11.165 -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')
11.166 -mv -f $MOVE doc
11.167 -rm doc/Isa-logics.eps
11.168 -rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
11.169 -rm -rf doc-src
11.170 -
11.171 -mkdir -p contrib
11.172 -cat >contrib/README <<EOF
11.173 -This directory contains add-on components that contribute to the main
11.174 -Isabelle distribution. Separate licensing conditions apply, see each
11.175 -directory individually.
11.176 -EOF
11.177 -
11.178 -cp doc/isabelle*.eps lib/logo
11.179 -
11.180 -if [ -z "$RELEASE" ]; then
11.181 - {
11.182 - echo
11.183 - echo "IMPORTANT NOTE"
11.184 - echo "=============="
11.185 - echo
11.186 - echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
11.187 - echo "See $REPOS/log/$IDENT for details."
11.188 - echo
11.189 - } >ANNOUNCE
11.190 -else
11.191 - perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
11.192 -fi
11.193 -
11.194 -perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
11.195 -perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
11.196 -perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
11.197 -perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
11.198 -perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
11.199 -perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
11.200 -
11.201 -
11.202 -# create archive
11.203 -
11.204 -echo "###"
11.205 -echo "### Creating archive ..."
11.206 -echo "###"
11.207 -
11.208 -cd "$DISTBASE"
11.209 -
11.210 -echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
11.211 -echo "$IDENT" >../ISABELLE_IDENT
11.212 -
11.213 -chown -R "$LOGNAME" "$DISTNAME"
11.214 -chmod -R u+w "$DISTNAME"
11.215 -chmod -R g=o "$DISTNAME"
11.216 -chgrp -R isabelle "$DISTNAME"
11.217 -
11.218 -echo "$DISTNAME.tar.gz"
11.219 -tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
11.220 -
11.221 -
11.222 -# cleanup dist
11.223 -
11.224 -mv "$DISTNAME" "${DISTNAME}-old"
11.225 -mkdir "$DISTNAME"
11.226 -
11.227 -mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
11.228 - "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
11.229 -mkdir "$DISTNAME/doc"
11.230 -mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
11.231 -
11.232 -rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
11.233 -
11.234 -chgrp -R isabelle "$DISTNAME"
11.235 -
11.236 -rm -rf "${DISTNAME}-old"
11.237 -
11.238 -echo "DONE"
12.1 --- a/Admin/mira.py Thu Jul 05 13:35:46 2012 +0200
12.2 +++ b/Admin/mira.py Thu Jul 05 14:13:14 2012 +0200
12.3 @@ -313,7 +313,7 @@
12.4 """Build of distribution"""
12.5 ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
12.6 isabelle_home = paths[0]
12.7 - (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'makedist'),
12.8 + (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'),
12.9 REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
12.10 return (return_code == 0, '', ## FIXME might add summary here
12.11 {}, {'log': log}, None) ## FIXME might add proper result here
13.1 --- a/Admin/mirror-website Thu Jul 05 13:35:46 2012 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,21 +0,0 @@
13.4 -#!/usr/bin/env bash
13.5 -#
13.6 -# mirrors the Isabelle website
13.7 -
13.8 -HOST=$(hostname)
13.9 -
13.10 -case ${HOST} in
13.11 - sunbroy* | atbroy* | macbroy*)
13.12 - DEST=/home/html/isabelle/html-data
13.13 - ;;
13.14 - *.cl.cam.ac.uk)
13.15 - USER=paulson
13.16 - DEST=/anfs/www/html/research/hvg/Isabelle
13.17 - ;;
13.18 - *)
13.19 - echo "Unknown destination directory for ${HOST}"
13.20 - exit 2
13.21 - ;;
13.22 -esac
13.23 -
13.24 -exec $(dirname $0)/isasync $DEST