3 # Author: Markus Wenzel, TU Muenchen
5 # build - compile the Isabelle system and object-logics
8 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
9 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
15 ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
20 PRG="$(basename "$0")"
22 ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
23 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
25 ISABELLE_OUTPUT="$ISABELLE_HOME/heaps/$ML_IDENTIFIER"
26 ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
34 echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
39 echo " -i make images"
40 echo " -m TARGET make this target"
43 echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
44 echo " in the distribution."
56 ## process command line
64 while getopts "abim:t" OPT
74 TARGETS="$TARGETS images"
77 TARGETS="$TARGETS $OPTARG"
80 TARGETS="$TARGETS test"
88 shift $(($OPTIND - 1))
95 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
96 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
101 # tell the user about current values
103 if [ -z "$BATCH" ]; then
105 echo " *****************************"
106 echo " * Welcome to Isabelle build *"
107 echo " *****************************"
109 echo "Please check $ISABELLE_HOME/etc/settings"
110 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
111 echo "to make sure that Isabelle's ML system settings and compilation options"
112 echo "are appropriate."
114 echo "The current values are:"
116 echo " ML_SYSTEM=$ML_SYSTEM"
117 echo " ML_HOME=$ML_HOME"
118 echo " ML_OPTIONS=$ML_OPTIONS"
119 echo " ML_PLATFORM=$ML_PLATFORM"
121 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
127 if [ -z "$BATCH" ]; then
130 echo "Press RETURN to compilation of"
139 DIR="$ISABELLE_HOME/src/$L"
140 if [ -f "$DIR/IsaMakefile" ]; then
141 MAKE_LOGICS="$MAKE_LOGICS $L"
143 echo "No such logic: $L"
148 if [ -z "$BATCH" ]; then
150 [ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
155 echo "Isabelle build: $MAKE_LOGICS"
156 [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
158 echo "ML_SYSTEM=$ML_SYSTEM"
159 echo "ML_HOME=$ML_HOME"
160 echo "ML_OPTIONS=$ML_OPTIONS"
161 echo "ML_PLATFORM=$ML_PLATFORM"
163 echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
170 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
171 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
173 for L in $MAKE_LOGICS
175 ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
178 echo -n "Finished at "; date
180 . "$ISABELLE_HOME/lib/scripts/timestop.bash"