|
1 #! /bin/sh |
|
2 # |
|
3 #make-all: make all systems afresh |
|
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 |
|
57 on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP) |
|
58 esac |
|
59 |
|
60 echo |
|
61 echo |
|
62 echo '*****Pure Isabelle*****' |
|
63 (cd Pure; make $NO > make$$.log) |
|
64 tail Pure/make$$.log |
|
65 gzip Pure/make$$.log |
|
66 |
|
67 echo |
|
68 echo |
|
69 echo '*****First-Order Logic (FOL)*****' |
|
70 (cd FOL; make $NO $TEST > make$$.log) |
|
71 tail FOL/make$$.log |
|
72 gzip FOL/make$$.log |
|
73 #cannot delete FOL yet... it is needed for ZF, CCL and LCF! |
|
74 |
|
75 echo |
|
76 echo |
|
77 echo '*****Set theory (ZF)*****' |
|
78 (cd ZF; make $NO $TEST > make$$.log) |
|
79 tail ZF/make$$.log |
|
80 gzip ZF/make$$.log |
|
81 case $CLEAN.$EXEC in |
|
82 on.on) rm $ISABELLEBIN/ZF |
|
83 esac |
|
84 |
|
85 echo |
|
86 echo |
|
87 echo '*****Classical Computational Logic (CCL)*****' |
|
88 (cd CCL; make $NO $TEST > make$$.log) |
|
89 tail CCL/make$$.log |
|
90 gzip CCL/make$$.log |
|
91 case $CLEAN.$EXEC in |
|
92 on.on) rm $ISABELLEBIN/CCL |
|
93 esac |
|
94 |
|
95 echo |
|
96 echo |
|
97 echo '*****Domain Theory (LCF)*****' |
|
98 (cd LCF; make $NO $TEST > make$$.log) |
|
99 tail LCF/make$$.log |
|
100 gzip LCF/make$$.log |
|
101 case $CLEAN.$EXEC in |
|
102 on.on) rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF |
|
103 esac |
|
104 |
|
105 echo |
|
106 echo |
|
107 echo '*****Constructive Type Theory (CTT)*****' |
|
108 (cd CTT; make $NO $TEST > make$$.log) |
|
109 tail CTT/make$$.log |
|
110 gzip CTT/make$$.log |
|
111 case $CLEAN.$EXEC in |
|
112 on.on) rm $ISABELLEBIN/CTT |
|
113 esac |
|
114 |
|
115 echo |
|
116 echo |
|
117 echo '*****Classical Sequent Calculus (LK)*****' |
|
118 (cd LK; make $NO $TEST > make$$.log) |
|
119 tail LK/make$$.log |
|
120 gzip LK/make$$.log |
|
121 #cannot delete LK yet... it is needed for Modal! |
|
122 |
|
123 echo |
|
124 echo |
|
125 echo '*****Modal logic (Modal)*****' |
|
126 (cd Modal; make $NO $TEST > make$$.log) |
|
127 tail Modal/make$$.log |
|
128 gzip Modal/make$$.log |
|
129 case $CLEAN.$EXEC in |
|
130 on.on) rm $ISABELLEBIN/LK $ISABELLEBIN/Modal |
|
131 esac |
|
132 |
|
133 echo |
|
134 echo |
|
135 echo '*****Higher-Order Logic (HOL)*****' |
|
136 (cd HOL; make $NO $TEST > make$$.log) |
|
137 tail HOL/make$$.log |
|
138 gzip HOL/make$$.log |
|
139 case $CLEAN.$EXEC in |
|
140 on.on) rm $ISABELLEBIN/HOL |
|
141 esac |
|
142 |
|
143 echo |
|
144 echo |
|
145 echo '*****The Lambda-Cube (Cube)*****' |
|
146 (cd Cube; make $NO $TEST > make$$.log) |
|
147 case $CLEAN.$EXEC in |
|
148 on.on) rm $ISABELLEBIN/Cube |
|
149 esac |
|
150 tail Cube/make$$.log |
|
151 gzip Cube/make$$.log |
|
152 |
|
153 echo |
|
154 echo |
|
155 echo '*****First-Order Logic with Proof Terms (FOLP)*****' |
|
156 (cd FOLP; make $NO $TEST > make$$.log) |
|
157 case $CLEAN.$EXEC in |
|
158 on.on) rm $ISABELLEBIN/FOLP |
|
159 esac |
|
160 tail FOLP/make$$.log |
|
161 gzip FOLP/make$$.log |
|
162 |
|
163 case $TEST.$EXEC in |
|
164 test.on) echo |
|
165 echo '***** Now check the dates on the "test" files *****' |
|
166 ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\ |
|
167 LK/test Modal/test HOL/test Cube/test FOLP/test |
|
168 esac |
|
169 echo Finished at `date` |