--- a/lib/Tools/makeall Fri Dec 19 12:09:08 1997 +0100
+++ b/lib/Tools/makeall Fri Dec 19 12:09:58 1997 +0100
@@ -2,181 +2,42 @@
#
# $Id$
#
-# DESCRIPTION: make all Isabelle systems afresh
-#
-# FIXME TODO:
-# - remove this tool (!?)
-# - clean
-# - usage
-# - getopts (i.e. *short* options) (?)
-
-
-# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
-# displays the last few lines of these files -- this indicates whether
-# the make failed (whether it terminated due to an error)
-
-# switches are
-# -noforce don't delete old databases/images first
-# -clean delete databases/images after use (leaving Pure)
-# -notest make databases/images w/o running the examples
-# -noexec don't execute, just check settings and IsaMakefiles
-
+# DESCRIPTION: apply make utility to all logics
-set -e #fail immediately upon errors
+## global settings
-# process command line switches
-CLEAN="off";
-FORCE="on";
-TEST="test";
-EXEC="on";
-NO="";
-for A in $*
-do
- case $A in
- -clean) CLEAN="on" ;;
- -noforce) FORCE="off" ;;
- -notest) TEST="" ;;
- -noexec) EXEC="off"
- NO="-n" ;;
- *) echo "Bad flag for makeall: $A"
- echo "Usage: makeall [-noforce] [-clean] [-notest] [-noexec]"
- exit ;;
- esac
-done
+ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
-echo Started at `date`
-echo Source=`pwd`
-echo Destination=$ISABELLE_OUTPUT
-echo force=$FORCE ' ' clean=$CLEAN ' '
-echo Compiler=$ML_SYSTEM
-echo Running on `hostname`
-echo Log files will be called make$$.log.gz
-case $TEST in
- test) echo; echo ' **** Full test: WILL TAKE MANY HOURS ****'
- echo ' **** Consider the -notest switch ****'
-esac
+## diagnostics
-mkdir -p $ISABELLE_OUTPUT
-
-case $FORCE.$EXEC in
- on.on) (cd $ISABELLE_OUTPUT;
- for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP IOA TLA
- do
- rm -f $f
- done)
-esac
-
-set +e #no longer fail upon errors -- e.g. if a make fails
+PRG=$(basename $0)
-echo
-echo
-echo '*****Pure Isabelle*****'
-( cd Pure; $ISATOOL make $NO > make$$.log )
-tail Pure/make$$.log
-gzip Pure/make$$.log
-
-echo
-echo
-echo '*****First-Order Logic (FOL)*****'
-(cd FOL; $ISATOOL make $NO $TEST > make$$.log)
-tail FOL/make$$.log
-gzip FOL/make$$.log
-#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
+function usage()
+{
+ echo
+ echo "Usage: $PRG [ARGS ...]"
+ echo
+ echo " Apply isatool make to all logics (passing ARGS)."
+ echo
+ exit 1
+}
-echo
-echo
-echo '*****Set theory (ZF)*****'
-(cd ZF; $ISATOOL make $NO $TEST > make$$.log)
-tail ZF/make$$.log
-gzip ZF/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/ZF
-esac
-
-echo
-echo
-echo '*****Classical Computational Logic (CCL)*****'
-(cd CCL; $ISATOOL make $NO $TEST > make$$.log)
-tail CCL/make$$.log
-gzip CCL/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/CCL
-esac
-echo
-echo
-echo '*****Domain Theory (LCF)*****'
-(cd LCF; $ISATOOL make $NO $TEST > make$$.log)
-tail LCF/make$$.log
-gzip LCF/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/FOL $ISABELLE_OUTPUT/LCF
-esac
+## main
+
+[ "$1" = "-?" ] && usage
-echo
-echo
-echo '*****Constructive Type Theory (CTT)*****'
-(cd CTT; $ISATOOL make $NO $TEST > make$$.log)
-tail CTT/make$$.log
-gzip CTT/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/CTT
-esac
-echo
-echo
-echo '*****Sequent Calculi (Sequents)*****'
-(cd Sequents; $ISATOOL make $NO $TEST > make$$.log)
-tail Sequents/make$$.log
-gzip Sequents/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/Sequents
-esac
-
-echo
-echo
-echo '*****Higher-Order Logic (HOL)*****'
-(cd HOL; $ISATOOL make $NO $TEST > make$$.log)
-tail HOL/make$$.log
-gzip HOL/make$$.log
-#cannot delete HOL yet... it is needed for HOLCF!
+SECONDS=0
+echo -n "Started at "; date
-echo
-echo
-echo '*****LCF in HOL (HOLCF)*****'
-(cd HOLCF; $ISATOOL make $NO $TEST > make$$.log)
-tail HOLCF/make$$.log
-gzip HOLCF/make$$.log
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/HOL $ISABELLE_OUTPUT/HOLCF
-esac
+for L in $ALL_LOGICS
+do
+ ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
+done
-echo
-echo
-echo '*****The Lambda-Cube (Cube)*****'
-(cd Cube; $ISATOOL make $NO $TEST > make$$.log)
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/Cube
-esac
-tail Cube/make$$.log
-gzip Cube/make$$.log
+echo -n "Finished at "; date
-echo
-echo
-echo '*****First-Order Logic with Proof Terms (FOLP)*****'
-(cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
-case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT/FOLP
-esac
-tail FOLP/make$$.log
-gzip FOLP/make$$.log
-
-case $TEST.$EXEC in
- test.on) echo
- echo '***** Now check the dates on the "test" files *****'
- ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
- Sequents/test HOL/test HOLCF/test\
- Cube/test FOLP/test
-esac
-echo Finished at `date`
+ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
+echo "$ELAPSED total elapsed time"