--- a/Admin/Release/CHECKLIST Sat Jul 28 20:12:47 2012 +0200
+++ b/Admin/Release/CHECKLIST Sat Jul 28 20:18:15 2012 +0200
@@ -31,7 +31,6 @@
doc/Contents
- maintain Logics:
- build
etc/components
lib/html/library_index_content.template
--- a/NEWS Sat Jul 28 20:12:47 2012 +0200
+++ b/NEWS Sat Jul 28 20:18:15 2012 +0200
@@ -73,6 +73,11 @@
build" tool and its examples. Eventual INCOMPATIBILITY, as isabelle
usedir / make / makeall are rendered obsolete.
+* Discontinued obsolete Isabelle/build script, it is superseded by the
+regular isabelle build tool. For example:
+
+ isabelle build -s -b HOLCF
+
* Discontinued support for Poly/ML 5.2.1, which was the last version
without exception positions and advanced ML compiler/toplevel
configuration.
--- a/build Sat Jul 28 20:12:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,181 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# build - compile the Isabelle system and object-logics
-
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-## global settings
-
-ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP LCF Sequents"
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-ISABELLE_OUTPUT="$ISABELLE_HOME/heaps/$ML_IDENTIFIER"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
- echo
- echo " Options are:"
- echo " -a all logics"
- echo " -b batch mode"
- echo " -i make images"
- echo " -m TARGET make this target"
- echo " -t make test"
- echo
- echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
- echo " in the distribution."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-ALL=""
-BATCH=""
-TARGETS=""
-
-while getopts "abim:t" OPT
-do
- case "$OPT" in
- a)
- ALL=true
- ;;
- b)
- BATCH=true
- ;;
- i)
- TARGETS="$TARGETS images"
- ;;
- m)
- TARGETS="$TARGETS $OPTARG"
- ;;
- t)
- TARGETS="$TARGETS test"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-LOGICS="$@"
-
-[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
-[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
-
-
-## main
-
-# tell the user about current values
-
-if [ -z "$BATCH" ]; then
- echo
- echo " *****************************"
- echo " * Welcome to Isabelle build *"
- echo " *****************************"
- echo
- echo "Please check $ISABELLE_HOME/etc/settings"
- [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
- echo "to make sure that Isabelle's ML system settings and compilation options"
- echo "are appropriate."
- echo
- echo "The current values are:"
- echo
- echo " ML_SYSTEM=$ML_SYSTEM"
- echo " ML_HOME=$ML_HOME"
- echo " ML_OPTIONS=$ML_OPTIONS"
- echo " ML_PLATFORM=$ML_PLATFORM"
- echo
- echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
-fi
-
-
-# check logics
-
-if [ -z "$BATCH" ]; then
- echo
- echo
- echo "Press RETURN to compilation of"
- echo
-fi
-
-
-MAKE_LOGICS=""
-
-for L in $LOGICS
-do
- DIR="$ISABELLE_HOME/src/$L"
- if [ -f "$DIR/IsaMakefile" ]; then
- MAKE_LOGICS="$MAKE_LOGICS $L"
- else
- echo "No such logic: $L"
- fi
-done
-
-
-if [ -z "$BATCH" ]; then
- echo " $MAKE_LOGICS"
- [ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
- echo
- read
-else
- echo
- echo "Isabelle build: $MAKE_LOGICS"
- [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
- echo
- echo "ML_SYSTEM=$ML_SYSTEM"
- echo "ML_HOME=$ML_HOME"
- echo "ML_OPTIONS=$ML_OPTIONS"
- echo "ML_PLATFORM=$ML_PLATFORM"
- echo
- echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
- echo
-fi
-
-
-# build it
-
-echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-for L in $MAKE_LOGICS
-do
- ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
-done
-
-echo -n "Finished at "; date
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-echo "$TIMES_REPORT"