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