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