4 # Author: Markus Wenzel, TU Muenchen
6 # build - compile the Isabelle system and object-logics
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
10 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
16 ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
21 PRG="$(basename "$0")"
23 ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
24 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
26 ISABELLE_OUTPUT="$ISABELLE_HOME/heaps/$ML_IDENTIFIER"
27 ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
35 echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
40 echo " -i make images"
41 echo " -m TARGET make this target"
44 echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
45 echo " in the distribution."
57 ## process command line
65 while getopts "abim:t" OPT
75 TARGETS="$TARGETS images"
78 TARGETS="$TARGETS $OPTARG"
81 TARGETS="$TARGETS test"
89 shift $(($OPTIND - 1))
96 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
97 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
102 # tell the user about current values
104 if [ -z "$BATCH" ]; then
106 echo " *****************************"
107 echo " * Welcome to Isabelle build *"
108 echo " *****************************"
110 echo "Please check $ISABELLE_HOME/etc/settings"
111 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
112 echo "to make sure that Isabelle's ML system settings and compilation options"
113 echo "are appropriate."
115 echo "The current values are:"
117 echo " ML_SYSTEM=$ML_SYSTEM"
118 echo " ML_HOME=$ML_HOME"
119 echo " ML_OPTIONS=$ML_OPTIONS"
120 echo " ML_PLATFORM=$ML_PLATFORM"
122 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
123 echo " HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
129 if [ -z "$BATCH" ]; then
132 echo "Press RETURN to compilation of"
141 DIR="$ISABELLE_HOME/src/$L"
142 if [ -f "$DIR/IsaMakefile" ]; then
143 MAKE_LOGICS="$MAKE_LOGICS $L"
145 echo "No such logic: $L"
150 if [ -z "$BATCH" ]; then
152 [ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
157 echo "Isabelle build: $MAKE_LOGICS"
158 [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
160 echo "ML_SYSTEM=$ML_SYSTEM"
161 echo "ML_HOME=$ML_HOME"
162 echo "ML_OPTIONS=$ML_OPTIONS"
163 echo "ML_PLATFORM=$ML_PLATFORM"
165 echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
166 echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
173 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
174 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
176 for L in $MAKE_LOGICS
178 ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
181 echo -n "Finished at "; date
183 . "$ISABELLE_HOME/lib/scripts/timestop.bash"