make-all
author lcp
Fri, 21 Oct 1994 09:47:02 +0100
changeset 649 237fce674bfb
parent 262 024b242bc26f
permissions -rwxr-xr-x
LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#! /bin/sh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
#make-all: make all systems afresh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
# displays the last few lines of these files -- this indicates whether
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
# the "make" failed (whether it terminated due to an error)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
# switches are
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#     -noforce	don't delete old databases/images first
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
#     -clean	delete databases/images after use (leaving Pure)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
#     -notest	make databases/images w/o running the examples
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
#     -noexec	don't execute, just check settings and Makefiles
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
#Environment variables required:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
# ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
# ISABELLECOMP: the ML compiler
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
# A typical shell script for /bin/sh is...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
# ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
# ISABELLEBIN=/homes/`whoami`/bin
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
# ISABELLECOMP="poly -noDisplay"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
# export ML_DBASE ISABELLEBIN ISABELLECOMP 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
# nohup make-all $*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
set -e			#fail immediately upon errors
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
# process command line switches
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
CLEAN="off";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
FORCE="on";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
TEST="test";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
EXEC="on";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
NO="";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
for A in $*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
do
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
	case $A in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
	-clean) CLEAN="on" ;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
	-noforce) FORCE="off" ;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
	-notest) TEST="" ;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
	-noexec) EXEC="off"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
                 NO="-n" ;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
	*)	echo "Bad flag for make-all: $A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
		echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
		exit ;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
	esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
done
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
echo Started at `date`
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
echo Source=`pwd`
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
echo Destination=${ISABELLEBIN?'No destination directory specified'}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
echo force=$FORCE '    ' clean=$CLEAN '    '
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
echo Compiler=${ISABELLECOMP?'No compiler specified'} 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
echo Running on `hostname`
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
echo Log files will be called make$$.log.gz
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
case $FORCE.$EXEC in
246
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
    57
    on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
9
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents: 0
diff changeset
    60
set +e			#no longer fail upon errors -- e.g. if a "make" fails
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents: 0
diff changeset
    61
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
echo '*****Pure Isabelle*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(cd Pure; make $NO > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
tail Pure/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
gzip Pure/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
echo '*****First-Order Logic (FOL)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(cd FOL;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
tail FOL/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
gzip FOL/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
echo '*****Set theory (ZF)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(cd ZF;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
tail ZF/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
gzip ZF/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
    on.on)	rm $ISABELLEBIN/ZF
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
echo '*****Classical Computational Logic (CCL)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(cd CCL;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
tail CCL/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
gzip CCL/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
    on.on)	rm $ISABELLEBIN/CCL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
echo '*****Domain Theory (LCF)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(cd LCF;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
tail LCF/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
gzip LCF/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
    on.on)	rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
echo '*****Constructive Type Theory (CTT)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(cd CTT;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
tail CTT/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
gzip CTT/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
    on.on)	rm $ISABELLEBIN/CTT
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
echo '*****Classical Sequent Calculus (LK)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
(cd LK;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
tail LK/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
gzip LK/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
#cannot delete LK yet... it is needed for Modal!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
echo '*****Modal logic (Modal)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(cd Modal;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
tail Modal/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
gzip Modal/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    on.on)	rm $ISABELLEBIN/LK $ISABELLEBIN/Modal
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
echo '*****Higher-Order Logic (HOL)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
(cd HOL;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
tail HOL/make$$.log
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
gzip HOL/make$$.log
246
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   141
#cannot delete HOL yet... it is needed for HOLCF!
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   142
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   143
echo
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   144
echo
262
024b242bc26f now makes HOLCF
lcp
parents: 246
diff changeset
   145
echo '*****LCF in HOL (HOLCF)*****'
246
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   146
(cd HOLCF;  make $NO $TEST > make$$.log)
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   147
tail HOLCF/make$$.log
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   148
gzip HOLCF/make$$.log
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
case $CLEAN.$EXEC in
246
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   150
    on.on)	rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
echo '*****The Lambda-Cube (Cube)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
(cd Cube;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
    on.on)	rm $ISABELLEBIN/Cube
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
tail Cube/make$$.log 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
gzip Cube/make$$.log 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(cd FOLP;  make $NO $TEST > make$$.log)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
case $CLEAN.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
    on.on)	rm $ISABELLEBIN/FOLP
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
tail FOLP/make$$.log 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
gzip FOLP/make$$.log 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
case $TEST.$EXEC in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
    test.on)	echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
	        echo '***** Now check the dates on the "test" files *****'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
        	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
246
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   177
              	        LK/test Modal/test HOL/test HOLCF/test Cube/test\
e5d184710a0b added HOLCF
nipkow
parents: 9
diff changeset
   178
                        FOLP/test
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
esac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
echo Finished at `date`