make-all

Addition of wrappers for integration with the simplifier.
New infixes setwrapper compwrapper addbefore addafter. New function
getwrapper. The wrapper is a tactical that is applied to the step tactic. By
default it is the identity. Using THEN one can cause other tactics to be
tried before or after the step tactic. Other effects are possible using
ORELSE, etc.

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