discontinued obsolete Isabelle/build script;
authorwenzelm
Sat, 28 Jul 2012 20:18:15 +0200
changeset 48586 500c6eb6c6dc
parent 48585 a82910dd2270
child 48587 f9732774ffc7
discontinued obsolete Isabelle/build script;
Admin/Release/CHECKLIST
NEWS
build
--- 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"