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