5 # build - compile the Isabelle system and object-logics
12 ISABELLE_HOME=$(dirname $0)
13 . $ISABELLE_HOME/lib/scripts/getsettings || \
14 { echo "$PRG probably not called from its original place!"; exit 2; }
22 echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
29 echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
30 echo " in the distribution."
42 ## process command line
50 while getopts "abt" OPT
68 shift $(($OPTIND - 1))
78 # tell the user about current values
80 if [ -z "$BATCH" ]; then
82 echo " *****************************"
83 echo " * Welcome to Isabelle build *"
84 echo " *****************************"
86 echo "Please check $ISABELLE_HOME/etc/settings"
87 [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
88 echo "to make sure that Isabelle's ML system settings are appropriate."
90 echo "Your current values are:"
92 echo " ML_SYSTEM=$ML_SYSTEM"
93 echo " ML_HOME=$ML_HOME"
94 echo " ML_OPTIONS=$ML_OPTIONS"
100 if [ -z "$BATCH" ]; then
103 echo "Press RETURN to start compilation (including parents) of:"
107 [ -z "$LOGICS" ] && LOGICS=$ISABELLE_LOGIC
109 if [ -n "$ALL" ]; then
111 for DIR in $ISABELLE_HOME/src/*
113 if [ -f $DIR/IsaMakefile ]; then
121 DIR=$ISABELLE_HOME/src/$L
122 [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
126 if [ -z "$BATCH" ]; then
132 echo "Isabelle build:" $LOGICS
134 echo "ML_SYSTEM=$ML_SYSTEM"
135 echo "ML_HOME=$ML_HOME"
136 echo "ML_OPTIONS=$ML_OPTIONS"
144 echo -n "Started at "; date
147 export THIS_IS_ISABELLE_BUILD=true
151 ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
155 echo -n "Finished at "; date