lib/Tools/makeall
author wenzelm
Tue Apr 22 11:37:12 1997 +0200 (1997-04-22)
changeset 3007 e5efa177ee0c
parent 2940 baae674b1d29
child 3118 24dae6222579
permissions -rwxr-xr-x
removed -norc;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: make all Isabelle systems afresh
     6 #
     7 # FIXME TODO:
     8 #  - remove this tool (!?)
     9 #  - clean
    10 #  - usage
    11 #  - getopts (i.e. *short* options) (?)
    12 
    13 
    14 # Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
    15 # displays the last few lines of these files -- this indicates whether
    16 # the make failed (whether it terminated due to an error)
    17 
    18 # switches are
    19 #     -noforce	don't delete old databases/images first
    20 #     -clean	delete databases/images after use (leaving Pure)
    21 #     -notest	make databases/images w/o running the examples
    22 #     -noexec	don't execute, just check settings and IsaMakefiles
    23 
    24 
    25 set -e			#fail immediately upon errors
    26 
    27 # process command line switches
    28 CLEAN="off";
    29 FORCE="on";
    30 TEST="test";
    31 EXEC="on";
    32 NO="";
    33 for A in $*
    34 do
    35 	case $A in
    36 	-clean) CLEAN="on" ;;
    37 	-noforce) FORCE="off" ;;
    38 	-notest) TEST="" ;;
    39 	-noexec) EXEC="off"
    40                  NO="-n" ;;
    41 	*)	echo "Bad flag for makeall: $A"
    42 		echo "Usage: makeall [-noforce] [-clean] [-notest] [-noexec]"
    43 		exit ;;
    44 	esac
    45 done
    46 
    47 
    48 echo Started at `date`
    49 echo Source=`pwd`
    50 echo Destination=$ISABELLE_OUTPUT_DIR
    51 echo force=$FORCE '    ' clean=$CLEAN '    '
    52 echo Compiler=$ML_SYSTEM
    53 echo Running on `hostname`
    54 echo Log files will be called make$$.log.gz
    55 case $TEST in
    56   test) echo; echo '		**** Full test: WILL TAKE MANY HOURS ****'
    57         echo '		**** Consider the -notest switch ****'
    58 esac
    59 
    60 mkdir -p $ISABELLE_OUTPUT_DIR
    61 
    62 case $FORCE.$EXEC in
    63   on.on) (cd $ISABELLE_OUTPUT_DIR;
    64           for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
    65 	  do 
    66 	   rm -f $f
    67 	  done)
    68 esac
    69 
    70 set +e			#no longer fail upon errors -- e.g. if a make fails
    71 
    72 echo
    73 echo
    74 echo '*****Pure Isabelle*****'
    75 ( cd Pure; $ISATOOL make $NO > make$$.log )
    76 tail Pure/make$$.log
    77 gzip Pure/make$$.log
    78 
    79 echo
    80 echo
    81 echo '*****First-Order Logic (FOL)*****'
    82 (cd FOL; $ISATOOL make $NO $TEST > make$$.log)
    83 tail FOL/make$$.log
    84 gzip FOL/make$$.log
    85 #cannot delete FOL yet... it is needed for ZF, CCL and LCF!
    86 
    87 echo
    88 echo
    89 echo '*****Set theory (ZF)*****'
    90 (cd ZF; $ISATOOL make $NO $TEST > make$$.log)
    91 tail ZF/make$$.log
    92 gzip ZF/make$$.log
    93 case $CLEAN.$EXEC in
    94     on.on)	rm -f $ISABELLE_OUTPUT_DIR/ZF
    95 esac
    96 
    97 echo
    98 echo
    99 echo '*****Classical Computational Logic (CCL)*****'
   100 (cd CCL; $ISATOOL make $NO $TEST > make$$.log)
   101 tail CCL/make$$.log
   102 gzip CCL/make$$.log
   103 case $CLEAN.$EXEC in
   104     on.on)	rm -f $ISABELLE_OUTPUT_DIR/CCL
   105 esac
   106 
   107 echo
   108 echo
   109 echo '*****Domain Theory (LCF)*****'
   110 (cd LCF; $ISATOOL make $NO $TEST > make$$.log)
   111 tail LCF/make$$.log
   112 gzip LCF/make$$.log
   113 case $CLEAN.$EXEC in
   114   on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF
   115 esac
   116 
   117 echo
   118 echo
   119 echo '*****Constructive Type Theory (CTT)*****'
   120 (cd CTT; $ISATOOL make $NO $TEST > make$$.log)
   121 tail CTT/make$$.log
   122 gzip CTT/make$$.log
   123 case $CLEAN.$EXEC in
   124     on.on)	rm -f $ISABELLE_OUTPUT_DIR/CTT
   125 esac
   126 
   127 echo
   128 echo
   129 echo '*****Sequent Calculi (Sequents)*****'
   130 (cd Sequents; $ISATOOL make $NO $TEST > make$$.log)
   131 tail Sequents/make$$.log
   132 gzip Sequents/make$$.log
   133 case $CLEAN.$EXEC in
   134     on.on)	rm -f $ISABELLE_OUTPUT_DIR/Sequents
   135 esac
   136 
   137 echo
   138 echo
   139 echo '*****Higher-Order Logic (HOL)*****'
   140 (cd HOL; $ISATOOL make $NO $TEST > make$$.log)
   141 tail HOL/make$$.log
   142 gzip HOL/make$$.log
   143 #cannot delete HOL yet... it is needed for HOLCF!
   144 
   145 echo
   146 echo
   147 echo '*****LCF in HOL (HOLCF)*****'
   148 (cd HOLCF; $ISATOOL make $NO $TEST > make$$.log)
   149 tail HOLCF/make$$.log
   150 gzip HOLCF/make$$.log
   151 case $CLEAN.$EXEC in
   152   on.on)	rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF
   153 esac
   154 
   155 echo
   156 echo
   157 echo '*****The Lambda-Cube (Cube)*****'
   158 (cd Cube; $ISATOOL make $NO $TEST > make$$.log)
   159 case $CLEAN.$EXEC in
   160     on.on)	rm -f $ISABELLE_OUTPUT_DIR/Cube
   161 esac
   162 tail Cube/make$$.log 
   163 gzip Cube/make$$.log 
   164 
   165 echo
   166 echo
   167 echo '*****First-Order Logic with Proof Terms (FOLP)*****'
   168 (cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
   169 case $CLEAN.$EXEC in
   170     on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOLP
   171 esac
   172 tail FOLP/make$$.log 
   173 gzip FOLP/make$$.log 
   174 
   175 case $TEST.$EXEC in
   176     test.on)	echo
   177 	        echo '***** Now check the dates on the "test" files *****'
   178         	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
   179               	        Sequents/test HOL/test HOLCF/test\
   180                         Cube/test FOLP/test
   181 esac
   182 echo Finished at `date`