make-all
author wenzelm
Thu Nov 25 11:37:51 1993 +0100 (1993-11-25)
changeset 143 f8152ca36cd5
parent 9 c1795fac88c3
child 246 e5d184710a0b
permissions -rwxr-xr-x
Sign.extend: Syntax.extend now called with read_ty;
     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 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 case $CLEAN.$EXEC in
   142     on.on)	rm $ISABELLEBIN/HOL
   143 esac
   144 
   145 echo
   146 echo
   147 echo '*****The Lambda-Cube (Cube)*****'
   148 (cd Cube;  make $NO $TEST > make$$.log)
   149 case $CLEAN.$EXEC in
   150     on.on)	rm $ISABELLEBIN/Cube
   151 esac
   152 tail Cube/make$$.log 
   153 gzip Cube/make$$.log 
   154 
   155 echo
   156 echo
   157 echo '*****First-Order Logic with Proof Terms (FOLP)*****'
   158 (cd FOLP;  make $NO $TEST > make$$.log)
   159 case $CLEAN.$EXEC in
   160     on.on)	rm $ISABELLEBIN/FOLP
   161 esac
   162 tail FOLP/make$$.log 
   163 gzip FOLP/make$$.log 
   164 
   165 case $TEST.$EXEC in
   166     test.on)	echo
   167 	        echo '***** Now check the dates on the "test" files *****'
   168         	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
   169               	        LK/test Modal/test HOL/test Cube/test FOLP/test
   170 esac
   171 echo Finished at `date`