#! /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`