author | clasohm |
Tue, 13 Jun 1995 13:38:54 +0200 | |
changeset 1146 | 75caf28a3aa9 |
parent 820 | 11e4827b3d75 |
child 1166 | def4ee9e116d |
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 |
|
1146 | 57 |
on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL CHOL HOLCF Cube FOLP) |
0 | 58 |
esac |
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 | 62 |
echo |
63 |
echo |
|
64 |
echo '*****Pure Isabelle*****' |
|
65 |
(cd Pure; make $NO > make$$.log) |
|
66 |
tail Pure/make$$.log |
|
67 |
gzip Pure/make$$.log |
|
68 |
||
69 |
echo |
|
70 |
echo |
|
71 |
echo '*****First-Order Logic (FOL)*****' |
|
72 |
(cd FOL; make $NO $TEST > make$$.log) |
|
73 |
tail FOL/make$$.log |
|
74 |
gzip FOL/make$$.log |
|
75 |
#cannot delete FOL yet... it is needed for ZF, CCL and LCF! |
|
76 |
||
77 |
echo |
|
78 |
echo |
|
79 |
echo '*****Set theory (ZF)*****' |
|
80 |
(cd ZF; make $NO $TEST > make$$.log) |
|
81 |
tail ZF/make$$.log |
|
82 |
gzip ZF/make$$.log |
|
83 |
case $CLEAN.$EXEC in |
|
84 |
on.on) rm $ISABELLEBIN/ZF |
|
85 |
esac |
|
86 |
||
87 |
echo |
|
88 |
echo |
|
89 |
echo '*****Classical Computational Logic (CCL)*****' |
|
90 |
(cd CCL; make $NO $TEST > make$$.log) |
|
91 |
tail CCL/make$$.log |
|
92 |
gzip CCL/make$$.log |
|