--- a/build Fri Dec 19 12:09:58 1997 +0100
+++ b/build Fri Dec 19 12:16:32 1997 +0100
@@ -5,6 +5,11 @@
# build - compile the Isabelle system and object-logics
+## global settings
+
+ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
+
+
## settings
PRG=$(basename $0)
@@ -72,6 +77,9 @@
LOGICS="$@"
+[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
+[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
+
## main
@@ -104,32 +112,27 @@
echo
fi
-[ -z "$LOGICS" ] && LOGICS=$ISABELLE_LOGIC
+
+MAKE_LOGICS=""
-if [ -n "$ALL" ]; then
- LOGICS=""
- for DIR in $ISABELLE_HOME/src/*
- do
- if [ -f $DIR/IsaMakefile ]; then
- L=$(basename $DIR)
- LOGICS="$LOGICS $L"
- fi
- done
-else
- for L in $LOGICS
- do
- DIR=$ISABELLE_HOME/src/$L
- [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
- done
-fi
+for L in $LOGICS
+do
+ DIR=$ISABELLE_HOME/src/$L
+ if [ -f $DIR/IsaMakefile ]; then
+ MAKE_LOGICS="$MAKE_LOGICS $L"
+ else
+ echo "No such logic: $L"
+ fi
+done
+
if [ -z "$BATCH" ]; then
- echo " " $LOGICS
+ echo " " $MAKE_LOGICS
echo
read
else
echo
- echo "Isabelle build:" $LOGICS
+ echo "Isabelle build:" $MAKE_LOGICS
echo
echo "ML_SYSTEM=$ML_SYSTEM"
echo "ML_HOME=$ML_HOME"
@@ -140,17 +143,17 @@
# build it
-echo
+SECONDS=0
echo -n "Started at "; date
-echo
export THIS_IS_ISABELLE_BUILD=true
-for L in $LOGICS
+for L in $MAKE_LOGICS
do
( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
done
-echo
echo -n "Finished at "; date
-echo
+
+ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
+echo "$ELAPSED total elapsed time"