1.1 --- a/Admin/Release/CHECKLIST Sat Jul 28 20:12:47 2012 +0200
1.2 +++ b/Admin/Release/CHECKLIST Sat Jul 28 20:18:15 2012 +0200
1.3 @@ -31,7 +31,6 @@
1.4 doc/Contents
1.5
1.6 - maintain Logics:
1.7 - build
1.8 etc/components
1.9 lib/html/library_index_content.template
1.10
2.1 --- a/NEWS Sat Jul 28 20:12:47 2012 +0200
2.2 +++ b/NEWS Sat Jul 28 20:18:15 2012 +0200
2.3 @@ -73,6 +73,11 @@
2.4 build" tool and its examples. Eventual INCOMPATIBILITY, as isabelle
2.5 usedir / make / makeall are rendered obsolete.
2.6
2.7 +* Discontinued obsolete Isabelle/build script, it is superseded by the
2.8 +regular isabelle build tool. For example:
2.9 +
2.10 + isabelle build -s -b HOLCF
2.11 +
2.12 * Discontinued support for Poly/ML 5.2.1, which was the last version
2.13 without exception positions and advanced ML compiler/toplevel
2.14 configuration.
3.1 --- a/build Sat Jul 28 20:12:47 2012 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,181 +0,0 @@
3.4 -#!/usr/bin/env bash
3.5 -#
3.6 -# Author: Markus Wenzel, TU Muenchen
3.7 -#
3.8 -# build - compile the Isabelle system and object-logics
3.9 -
3.10 -if [ -L "$0" ]; then
3.11 - TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
3.12 - exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
3.13 -fi
3.14 -
3.15 -
3.16 -## global settings
3.17 -
3.18 -ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP LCF Sequents"
3.19 -
3.20 -
3.21 -## settings
3.22 -
3.23 -PRG="$(basename "$0")"
3.24 -
3.25 -ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
3.26 -source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
3.27 -
3.28 -ISABELLE_OUTPUT="$ISABELLE_HOME/heaps/$ML_IDENTIFIER"
3.29 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
3.30 -
3.31 -
3.32 -## diagnostics
3.33 -
3.34 -function usage()
3.35 -{
3.36 - echo
3.37 - echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
3.38 - echo
3.39 - echo " Options are:"
3.40 - echo " -a all logics"
3.41 - echo " -b batch mode"
3.42 - echo " -i make images"
3.43 - echo " -m TARGET make this target"
3.44 - echo " -t make test"
3.45 - echo
3.46 - echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
3.47 - echo " in the distribution."
3.48 - echo
3.49 - exit 1
3.50 -}
3.51 -
3.52 -function fail()
3.53 -{
3.54 - echo "$1" >&2
3.55 - exit 2
3.56 -}
3.57 -
3.58 -
3.59 -## process command line
3.60 -
3.61 -# options
3.62 -
3.63 -ALL=""
3.64 -BATCH=""
3.65 -TARGETS=""
3.66 -
3.67 -while getopts "abim:t" OPT
3.68 -do
3.69 - case "$OPT" in
3.70 - a)
3.71 - ALL=true
3.72 - ;;
3.73 - b)
3.74 - BATCH=true
3.75 - ;;
3.76 - i)
3.77 - TARGETS="$TARGETS images"
3.78 - ;;
3.79 - m)
3.80 - TARGETS="$TARGETS $OPTARG"
3.81 - ;;
3.82 - t)
3.83 - TARGETS="$TARGETS test"
3.84 - ;;
3.85 - \?)
3.86 - usage
3.87 - ;;
3.88 - esac
3.89 -done
3.90 -
3.91 -shift $(($OPTIND - 1))
3.92 -
3.93 -
3.94 -# args
3.95 -
3.96 -LOGICS="$@"
3.97 -
3.98 -[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
3.99 -[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
3.100 -
3.101 -
3.102 -## main
3.103 -
3.104 -# tell the user about current values
3.105 -
3.106 -if [ -z "$BATCH" ]; then
3.107 - echo
3.108 - echo " *****************************"
3.109 - echo " * Welcome to Isabelle build *"
3.110 - echo " *****************************"
3.111 - echo
3.112 - echo "Please check $ISABELLE_HOME/etc/settings"
3.113 - [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
3.114 - echo "to make sure that Isabelle's ML system settings and compilation options"
3.115 - echo "are appropriate."
3.116 - echo
3.117 - echo "The current values are:"
3.118 - echo
3.119 - echo " ML_SYSTEM=$ML_SYSTEM"
3.120 - echo " ML_HOME=$ML_HOME"
3.121 - echo " ML_OPTIONS=$ML_OPTIONS"
3.122 - echo " ML_PLATFORM=$ML_PLATFORM"
3.123 - echo
3.124 - echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
3.125 -fi
3.126 -
3.127 -
3.128 -# check logics
3.129 -
3.130 -if [ -z "$BATCH" ]; then
3.131 - echo
3.132 - echo
3.133 - echo "Press RETURN to compilation of"
3.134 - echo
3.135 -fi
3.136 -
3.137 -
3.138 -MAKE_LOGICS=""
3.139 -
3.140 -for L in $LOGICS
3.141 -do
3.142 - DIR="$ISABELLE_HOME/src/$L"
3.143 - if [ -f "$DIR/IsaMakefile" ]; then
3.144 - MAKE_LOGICS="$MAKE_LOGICS $L"
3.145 - else
3.146 - echo "No such logic: $L"
3.147 - fi
3.148 -done
3.149 -
3.150 -
3.151 -if [ -z "$BATCH" ]; then
3.152 - echo " $MAKE_LOGICS"
3.153 - [ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
3.154 - echo
3.155 - read
3.156 -else
3.157 - echo
3.158 - echo "Isabelle build: $MAKE_LOGICS"
3.159 - [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
3.160 - echo
3.161 - echo "ML_SYSTEM=$ML_SYSTEM"
3.162 - echo "ML_HOME=$ML_HOME"
3.163 - echo "ML_OPTIONS=$ML_OPTIONS"
3.164 - echo "ML_PLATFORM=$ML_PLATFORM"
3.165 - echo
3.166 - echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
3.167 - echo
3.168 -fi
3.169 -
3.170 -
3.171 -# build it
3.172 -
3.173 -echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
3.174 -. "$ISABELLE_HOME/lib/scripts/timestart.bash"
3.175 -
3.176 -for L in $MAKE_LOGICS
3.177 -do
3.178 - ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
3.179 -done
3.180 -
3.181 -echo -n "Finished at "; date
3.182 -
3.183 -. "$ISABELLE_HOME/lib/scripts/timestop.bash"
3.184 -echo "$TIMES_REPORT"