make-all
author lcp
Fri Apr 15 18:34:26 1994 +0200 (1994-04-15)
changeset 328 2d1b460dbb62
parent 262 024b242bc26f
permissions -rwxr-xr-x
penultimate Springer draft
     1 #! /bin/sh
     2 #
     3 #make-all: make all systems afresh
     4 
     5 # Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
     6 # displays the last few lines of these files -- this indicates whether
     7 # the "make" failed (whether it terminated due to an error)
     8 
     9 # switches are
    10 #     -noforce	don't delete old databases/images first
    11 #     -clean	delete databases/images after use (leaving Pure)
    12 #     -notest	make databases/images w/o running the examples
    13 #     -noexec	don't execute, just check settings and Makefiles
    14 
    15 #Environment variables required:
    16 # ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images
    17 # ISABELLECOMP: the ML compiler
    18 
    19 # A typical shell script for /bin/sh is...
    20 # ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase
    21 # ISABELLEBIN=/homes/`whoami`/bin
    22 # ISABELLECOMP="poly -noDisplay"
    23 # export ML_DBASE ISABELLEBIN ISABELLECOMP 
    24 # nohup make-all $*
    25 
    26 set -e			#fail immediately upon errors
    27 
    28 # process command line switches
    29 CLEAN="off";
    30 FORCE="on";
    31 TEST="test";
    32 EXEC="on";
    33 NO="";
    34 for A in $*
    35 do
    36 	case $A in
    37 	-clean) CLEAN="on" ;;
    38 	-noforce) FORCE="off" ;;
    39 	-notest) TEST="" ;;
    40 	-noexec) EXEC="off"
    41                  NO="-n" ;;
    42 	*)	echo "Bad flag for make-all: $A"
    43 		echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]"
    44 		exit ;;
    45 	esac
    46 done
    47 
    48 echo Started at `date`
    49 echo Source=`pwd`
    50 echo Destination=${ISABELLEBIN?'No destination directory specified'}
    51 echo force=$FORCE '    ' clean=$CLEAN '    '
    52 echo Compiler=${ISABELLECOMP?'No compiler specified'} 
    53 echo Running on `hostname`
    54 echo Log files will be called make$$.log.gz
    55 
    56 case $FORCE.$EXEC in
    57     on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP)
    58 esac
    59 
    60 set +e			#no longer fail upon errors -- e.g. if a "make" fails
    61 
    62 echo
    63 echo
    64 echo '*****Pure Isabelle*****'
    65 (cd Pure; make $NO > make$$.log)
    66 tail Pure/make$$.log
    67 gzip Pure/make$$.log
    68 
    69 echo
    70 echo
    71 echo '*****First-Order Logic (FOL)*****'
    72 (cd FOL;  make $NO $TEST > make$$.log)
    73 tail FOL/make$$.log
    74 gzip FOL/make$$.log
    75 #cannot delete FOL yet... it is needed for ZF, CCL and LCF!
    76 
    77 echo
    78 echo
    79 echo '*****Set theory (ZF)*****'
    80 (cd ZF;  make $NO $TEST > make$$.log)
    81 tail ZF/make$$.log
    82 gzip ZF/make$$.log
    83 case $CLEAN.$EXEC in
    84     on.on)	rm $ISABELLEBIN/ZF
    85 esac
    86 
    87 echo
    88 echo
    89 echo '*****Classical Computational Logic (CCL)*****'
    90 (cd CCL;  make $NO $TEST > make$$.log)
    91 tail CCL/make$$.log
    92 gzip CCL/make$$.log
    93 case $CLEAN.$EXEC in
    94     on.on)	rm $ISABELLEBIN/CCL
    95 esac
    96 
    97 echo
    98 echo
    99 echo '*****Domain Theory (LCF)*****'
   100 (cd LCF;  make $NO $TEST > make$$.log)
   101 tail LCF/make$$.log
   102 gzip LCF/make$$.log
   103 case $CLEAN.$EXEC in
   104     on.on)	rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF
   105 esac
   106 
   107 echo
   108 echo
   109 echo '*****Constructive Type Theory (CTT)*****'
   110 (cd CTT;  make $NO $TEST > make$$.log)
   111 tail CTT/make$$.log
   112 gzip CTT/make$$.log
   113 case $CLEAN.$EXEC in
   114     on.on)	rm $ISABELLEBIN/CTT
   115 esac
   116 
   117 echo
   118 echo
   119 echo '*****Classical Sequent Calculus (LK)*****'
   120 (cd LK;  make $NO $TEST > make$$.log)
   121 tail LK/make$$.log
   122 gzip LK/make$$.log
   123 #cannot delete LK yet... it is needed for Modal!
   124 
   125 echo
   126 echo
   127 echo '*****Modal logic (Modal)*****'
   128 (cd Modal;  make $NO $TEST > make$$.log)
   129 tail Modal/make$$.log
   130 gzip Modal/make$$.log
   131 case $CLEAN.$EXEC in
   132     on.on)	rm $ISABELLEBIN/LK $ISABELLEBIN/Modal
   133 esac
   134 
   135 echo
   136 echo
   137 echo '*****Higher-Order Logic (HOL)*****'
   138 (cd HOL;  make $NO $TEST > make$$.log)
   139 tail HOL/make$$.log
   140 gzip HOL/make$$.log
   141 #cannot delete HOL yet... it is needed for HOLCF!
   142 
   143 echo
   144 echo
   145 echo '*****LCF in HOL (HOLCF)*****'
   146 (cd HOLCF;  make $NO $TEST > make$$.log)
   147 tail HOLCF/make$$.log
   148 gzip HOLCF/make$$.log
   149 case $CLEAN.$EXEC in
   150     on.on)	rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF
   151 esac
   152 
   153 echo
   154 echo
   155 echo '*****The Lambda-Cube (Cube)*****'
   156 (cd Cube;  make $NO $TEST > make$$.log)
   157 case $CLEAN.$EXEC in
   158     on.on)	rm $ISABELLEBIN/Cube
   159 esac
   160 tail Cube/make$$.log 
   161 gzip Cube/make$$.log 
   162 
   163 echo
   164 echo
   165 echo '*****First-Order Logic with Proof Terms (FOLP)*****'
   166 (cd FOLP;  make $NO $TEST > make$$.log)
   167 case $CLEAN.$EXEC in
   168     on.on)	rm $ISABELLEBIN/FOLP
   169 esac
   170 tail FOLP/make$$.log 
   171 gzip FOLP/make$$.log 
   172 
   173 case $TEST.$EXEC in
   174     test.on)	echo
   175 	        echo '***** Now check the dates on the "test" files *****'
   176         	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
   177               	        LK/test Modal/test HOL/test HOLCF/test Cube/test\
   178                         FOLP/test
   179 esac
   180 echo Finished at `date`