author | lcp |
Wed, 17 Aug 1994 10:38:37 +0200 | |
changeset 540 | e30c23731c2d |
parent 262 | 024b242bc26f |
permissions | -rwxr-xr-x |
#! /bin/sh # #make-all: make all systems afresh # 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 Makefiles #Environment variables required: # ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images # ISABELLECOMP: the ML compiler # A typical shell script for /bin/sh is... # ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase # ISABELLEBIN=/homes/`whoami`/bin # ISABELLECOMP="poly -noDisplay" # export ML_DBASE ISABELLEBIN ISABELLECOMP # nohup make-all $* set -e #fail immediately upon errors # 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 make-all: $A" echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]" exit ;; esac done echo Started at `date` echo Source=`pwd` echo Destination=${ISABELLEBIN?'No destination directory specified'} echo force=$FORCE ' ' clean=$CLEAN ' ' echo Compiler=${ISABELLECOMP?'No compiler specified'} echo Running on `hostname` echo Log files will be called make$$.log.gz case $FORCE.$EXEC in on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP) esac set +e #no longer fail upon errors -- e.g. if a "make" fails echo echo echo '*****Pure Isabelle*****' (cd Pure; make $NO > make$$.log) tail Pure/make$$.log gzip Pure/make$$.log echo echo echo '*****First-Order Logic (FOL)*****' (cd FOL; 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! echo echo echo '*****Set theory (ZF)*****' (cd ZF; make $NO $TEST > make$$.log) tail ZF/make$$.log gzip ZF/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/ZF esac echo echo echo '*****Classical Computational Logic (CCL)*****' (cd CCL; make $NO $TEST > make$$.log) tail CCL/make$$.log gzip CCL/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/CCL esac echo echo echo '*****Domain Theory (LCF)*****' (cd LCF; make $NO $TEST > make$$.log) tail LCF/make$$.log gzip LCF/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF esac echo echo echo '*****Constructive Type Theory (CTT)*****' (cd CTT; make $NO $TEST > make$$.log) tail CTT/make$$.log gzip CTT/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/CTT esac echo echo echo '*****Classical Sequent Calculus (LK)*****' (cd LK; make $NO $TEST > make$$.log) tail LK/make$$.log gzip LK/make$$.log #cannot delete LK yet... it is needed for Modal! echo echo echo '*****Modal logic (Modal)*****' (cd Modal; make $NO $TEST > make$$.log) tail Modal/make$$.log gzip Modal/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/LK $ISABELLEBIN/Modal esac echo echo echo '*****Higher-Order Logic (HOL)*****' (cd HOL; make $NO $TEST > make$$.log) tail HOL/make$$.log gzip HOL/make$$.log #cannot delete HOL yet... it is needed for HOLCF! echo echo echo '*****LCF in HOL (HOLCF)*****' (cd HOLCF; make $NO $TEST > make$$.log) tail HOLCF/make$$.log gzip HOLCF/make$$.log case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF esac echo echo echo '*****The Lambda-Cube (Cube)*****' (cd Cube; make $NO $TEST > make$$.log) case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/Cube esac tail Cube/make$$.log gzip Cube/make$$.log echo echo echo '*****First-Order Logic with Proof Terms (FOLP)*****' (cd FOLP; make $NO $TEST > make$$.log) case $CLEAN.$EXEC in on.on) rm $ISABELLEBIN/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\ LK/test Modal/test HOL/test HOLCF/test Cube/test\ FOLP/test esac echo Finished at `date`