diff -r 44e57a6d947d -r 6e6d99e06d0c build --- 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"