src/Tools/make-all
changeset 0 a5a9c433f639
child 9 c1795fac88c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/make-all	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,169 @@
     1.4 +#! /bin/sh
     1.5 +#
     1.6 +#make-all: make all systems afresh
     1.7 +
     1.8 +# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
     1.9 +# displays the last few lines of these files -- this indicates whether
    1.10 +# the "make" failed (whether it terminated due to an error)
    1.11 +
    1.12 +# switches are
    1.13 +#     -noforce	don't delete old databases/images first
    1.14 +#     -clean	delete databases/images after use (leaving Pure)
    1.15 +#     -notest	make databases/images w/o running the examples
    1.16 +#     -noexec	don't execute, just check settings and Makefiles
    1.17 +
    1.18 +#Environment variables required:
    1.19 +# ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images
    1.20 +# ISABELLECOMP: the ML compiler
    1.21 +
    1.22 +# A typical shell script for /bin/sh is...
    1.23 +# ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase
    1.24 +# ISABELLEBIN=/homes/`whoami`/bin
    1.25 +# ISABELLECOMP="poly -noDisplay"
    1.26 +# export ML_DBASE ISABELLEBIN ISABELLECOMP 
    1.27 +# nohup make-all $*
    1.28 +
    1.29 +set -e			#fail immediately upon errors
    1.30 +
    1.31 +# process command line switches
    1.32 +CLEAN="off";
    1.33 +FORCE="on";
    1.34 +TEST="test";
    1.35 +EXEC="on";
    1.36 +NO="";
    1.37 +for A in $*
    1.38 +do
    1.39 +	case $A in
    1.40 +	-clean) CLEAN="on" ;;
    1.41 +	-noforce) FORCE="off" ;;
    1.42 +	-notest) TEST="" ;;
    1.43 +	-noexec) EXEC="off"
    1.44 +                 NO="-n" ;;
    1.45 +	*)	echo "Bad flag for make-all: $A"
    1.46 +		echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]"
    1.47 +		exit ;;
    1.48 +	esac
    1.49 +done
    1.50 +
    1.51 +echo Started at `date`
    1.52 +echo Source=`pwd`
    1.53 +echo Destination=${ISABELLEBIN?'No destination directory specified'}
    1.54 +echo force=$FORCE '    ' clean=$CLEAN '    '
    1.55 +echo Compiler=${ISABELLECOMP?'No compiler specified'} 
    1.56 +echo Running on `hostname`
    1.57 +echo Log files will be called make$$.log.gz
    1.58 +
    1.59 +case $FORCE.$EXEC in
    1.60 +    on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP)
    1.61 +esac
    1.62 +
    1.63 +echo
    1.64 +echo
    1.65 +echo '*****Pure Isabelle*****'
    1.66 +(cd Pure; make $NO > make$$.log)
    1.67 +tail Pure/make$$.log
    1.68 +gzip Pure/make$$.log
    1.69 +
    1.70 +echo
    1.71 +echo
    1.72 +echo '*****First-Order Logic (FOL)*****'
    1.73 +(cd FOL;  make $NO $TEST > make$$.log)
    1.74 +tail FOL/make$$.log
    1.75 +gzip FOL/make$$.log
    1.76 +#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
    1.77 +
    1.78 +echo
    1.79 +echo
    1.80 +echo '*****Set theory (ZF)*****'
    1.81 +(cd ZF;  make $NO $TEST > make$$.log)
    1.82 +tail ZF/make$$.log
    1.83 +gzip ZF/make$$.log
    1.84 +case $CLEAN.$EXEC in
    1.85 +    on.on)	rm $ISABELLEBIN/ZF
    1.86 +esac
    1.87 +
    1.88 +echo
    1.89 +echo
    1.90 +echo '*****Classical Computational Logic (CCL)*****'
    1.91 +(cd CCL;  make $NO $TEST > make$$.log)
    1.92 +tail CCL/make$$.log
    1.93 +gzip CCL/make$$.log
    1.94 +case $CLEAN.$EXEC in
    1.95 +    on.on)	rm $ISABELLEBIN/CCL
    1.96 +esac
    1.97 +
    1.98 +echo
    1.99 +echo
   1.100 +echo '*****Domain Theory (LCF)*****'
   1.101 +(cd LCF;  make $NO $TEST > make$$.log)
   1.102 +tail LCF/make$$.log
   1.103 +gzip LCF/make$$.log
   1.104 +case $CLEAN.$EXEC in
   1.105 +    on.on)	rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF
   1.106 +esac
   1.107 +
   1.108 +echo
   1.109 +echo
   1.110 +echo '*****Constructive Type Theory (CTT)*****'
   1.111 +(cd CTT;  make $NO $TEST > make$$.log)
   1.112 +tail CTT/make$$.log
   1.113 +gzip CTT/make$$.log
   1.114 +case $CLEAN.$EXEC in
   1.115 +    on.on)	rm $ISABELLEBIN/CTT
   1.116 +esac
   1.117 +
   1.118 +echo
   1.119 +echo
   1.120 +echo '*****Classical Sequent Calculus (LK)*****'
   1.121 +(cd LK;  make $NO $TEST > make$$.log)
   1.122 +tail LK/make$$.log
   1.123 +gzip LK/make$$.log
   1.124 +#cannot delete LK yet... it is needed for Modal!
   1.125 +
   1.126 +echo
   1.127 +echo
   1.128 +echo '*****Modal logic (Modal)*****'
   1.129 +(cd Modal;  make $NO $TEST > make$$.log)
   1.130 +tail Modal/make$$.log
   1.131 +gzip Modal/make$$.log
   1.132 +case $CLEAN.$EXEC in
   1.133 +    on.on)	rm $ISABELLEBIN/LK $ISABELLEBIN/Modal
   1.134 +esac
   1.135 +
   1.136 +echo
   1.137 +echo
   1.138 +echo '*****Higher-Order Logic (HOL)*****'
   1.139 +(cd HOL;  make $NO $TEST > make$$.log)
   1.140 +tail HOL/make$$.log
   1.141 +gzip HOL/make$$.log
   1.142 +case $CLEAN.$EXEC in
   1.143 +    on.on)	rm $ISABELLEBIN/HOL
   1.144 +esac
   1.145 +
   1.146 +echo
   1.147 +echo
   1.148 +echo '*****The Lambda-Cube (Cube)*****'
   1.149 +(cd Cube;  make $NO $TEST > make$$.log)
   1.150 +case $CLEAN.$EXEC in
   1.151 +    on.on)	rm $ISABELLEBIN/Cube
   1.152 +esac
   1.153 +tail Cube/make$$.log 
   1.154 +gzip Cube/make$$.log 
   1.155 +
   1.156 +echo
   1.157 +echo
   1.158 +echo '*****First-Order Logic with Proof Terms (FOLP)*****'
   1.159 +(cd FOLP;  make $NO $TEST > make$$.log)
   1.160 +case $CLEAN.$EXEC in
   1.161 +    on.on)	rm $ISABELLEBIN/FOLP
   1.162 +esac
   1.163 +tail FOLP/make$$.log 
   1.164 +gzip FOLP/make$$.log 
   1.165 +
   1.166 +case $TEST.$EXEC in
   1.167 +    test.on)	echo
   1.168 +	        echo '***** Now check the dates on the "test" files *****'
   1.169 +        	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
   1.170 +              	        LK/test Modal/test HOL/test Cube/test FOLP/test
   1.171 +esac
   1.172 +echo Finished at `date`