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