wneuper/isa: lib/Tools/makeall@24dae6222579

     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) (?)

    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)

    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

    25 set -e			#fail immediately upon errors

    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

    48 echo Started at `date`

    49 echo Source=`pwd`

    50 echo Destination=$ISABELLE_OUTPUT

    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

    60 mkdir -p $ISABELLE_OUTPUT

    62 case $FORCE.$EXEC in

    63   on.on) (cd $ISABELLE_OUTPUT;

    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

    70 set +e			#no longer fail upon errors -- e.g. if a make fails

    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

    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!

    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/ZF

    95 esac

    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/CCL

   105 esac

   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/FOL $ISABELLE_OUTPUT/LCF

   115 esac

   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/CTT

   125 esac

   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/Sequents

   135 esac

   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!

   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/HOL $ISABELLE_OUTPUT/HOLCF

   153 esac

   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/Cube

   161 esac

   162 tail Cube/make$$.log

   163 gzip Cube/make$$.log

   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/FOLP

   171 esac

   172 tail FOLP/make$$.log

   173 gzip FOLP/make$$.log

   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`

author	wenzelm
	Tue, 06 May 1997 15:27:35 +0200
changeset 3118	24dae6222579
parent 3007	e5efa177ee0c
child 3957	7914990748ad
permissions	-rwxr-xr-x