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