lib/Tools/makeall
changeset 4456 44e57a6d947d
parent 3957 7914990748ad
child 7277 bb9502f9154a
equal deleted inserted replaced
4455:c0a6ad614fa0 4456:44e57a6d947d
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: make all Isabelle systems afresh
     5 # DESCRIPTION: apply make utility to all logics
     6 #
     6 
     7 # FIXME TODO:
     7 ## global settings
     8 #  - remove this tool (!?)
     8 
     9 #  - clean
     9 ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
    10 #  - usage
       
    11 #  - getopts (i.e. *short* options) (?)
       
    12 
    10 
    13 
    11 
    14 # Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
    12 ## diagnostics
    15 # displays the last few lines of these files -- this indicates whether
       
    16 # the make failed (whether it terminated due to an error)
       
    17 
    13 
    18 # switches are
    14 PRG=$(basename $0)
    19 #     -noforce	don't delete old databases/images first
    15 
    20 #     -clean	delete databases/images after use (leaving Pure)
    16 function usage()
    21 #     -notest	make databases/images w/o running the examples
    17 {
    22 #     -noexec	don't execute, just check settings and IsaMakefiles
    18   echo
       
    19   echo "Usage: $PRG [ARGS ...]"
       
    20   echo
       
    21   echo "  Apply isatool make to all logics (passing ARGS)."
       
    22   echo
       
    23   exit 1
       
    24 }
    23 
    25 
    24 
    26 
    25 set -e			#fail immediately upon errors
    27 ## main
    26 
    28 
    27 # process command line switches
    29 [ "$1" = "-?" ] && usage
    28 CLEAN="off";
    30 
    29 FORCE="on";
    31 
    30 TEST="test";
    32 SECONDS=0
    31 EXEC="on";
    33 echo -n "Started at "; date
    32 NO="";
    34 
    33 for A in $*
    35 for L in $ALL_LOGICS
    34 do
    36 do
    35 	case $A in
    37   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
    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
    38 done
    46 
    39 
       
    40 echo -n "Finished at "; date
    47 
    41 
    48 echo Started at `date`
    42 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
    49 echo Source=`pwd`
    43 echo "$ELAPSED total elapsed time"
    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
       
    59 
       
    60 mkdir -p $ISABELLE_OUTPUT
       
    61 
       
    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 IOA TLA
       
    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/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/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/FOL $ISABELLE_OUTPUT/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/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/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/HOL $ISABELLE_OUTPUT/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/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/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`