# HG changeset patch # User wenzelm # Date 1343499495 -7200 # Node ID 500c6eb6c6dcc1608ad31f4391ab2c6bd06b64fd # Parent a82910dd22700cb6371ed4f629a60ddb70868d51 discontinued obsolete Isabelle/build script; diff -r a82910dd2270 -r 500c6eb6c6dc Admin/Release/CHECKLIST --- 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 diff -r a82910dd2270 -r 500c6eb6c6dc NEWS --- 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. diff -r a82910dd2270 -r 500c6eb6c6dc build --- 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"