4 # Author: Markus Wenzel, TU Muenchen
6 # build - compile the Isabelle system and object-logics
11 ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
16 PRG="$(basename "$0")"
18 export THIS_IS_ISABELLE_BUILD=true
19 ISABELLE_HOME="$(dirname "$0")"
20 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
21 { echo "$PRG probably not called from its original place!"; exit 2; }
29 echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
34 echo " -i make images"
35 echo " -m TARGET make this target"
38 echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
39 echo " in the distribution."
51 ## process command line
59 while getopts "abim:p:t" OPT
69 TARGETS="$TARGETS images"
72 TARGETS="$TARGETS $OPTARG"
75 TARGETS="$TARGETS test"
83 shift $(($OPTIND - 1))
90 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
91 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
96 # tell the user about current values
98 if [ -z "$BATCH" ]; then
100 echo " *****************************"
101 echo " * Welcome to Isabelle build *"
102 echo " *****************************"
104 echo "Please check $ISABELLE_HOME/etc/settings"
105 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
106 echo "to make sure that Isabelle's ML system settings and compilation options"
107 echo "are appropriate."
109 echo "The current values are:"
111 echo " ML_SYSTEM=$ML_SYSTEM"
112 echo " ML_HOME=$ML_HOME"
113 echo " ML_OPTIONS=$ML_OPTIONS"
114 echo " ML_PLATFORM=$ML_PLATFORM"
116 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
122 if [ -z "$BATCH" ]; then
125 echo "Press RETURN to compilation of"
134 DIR="$ISABELLE_HOME/src/$L"
135 if [ -f "$DIR/IsaMakefile" ]; then
136 MAKE_LOGICS="$MAKE_LOGICS $L"
138 echo "No such logic: $L"
143 if [ -z "$BATCH" ]; then
145 [ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
150 echo "Isabelle build: $MAKE_LOGICS"
151 [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
153 echo "ML_SYSTEM=$ML_SYSTEM"
154 echo "ML_HOME=$ML_HOME"
155 echo "ML_OPTIONS=$ML_OPTIONS"
156 echo "ML_PLATFORM=$ML_PLATFORM"
158 echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
166 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
168 for L in $MAKE_LOGICS
170 ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
173 echo -n "Finished at "; date
175 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
176 echo "$ELAPSED total elapsed time"