#! /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 (HOL)*****'

 (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`