45 done |
45 done |
46 |
46 |
47 |
47 |
48 echo Started at `date` |
48 echo Started at `date` |
49 echo Source=`pwd` |
49 echo Source=`pwd` |
50 echo Destination=$ISABELLE_OUTPUT_DIR |
50 echo Destination=$ISABELLE_OUTPUT |
51 echo force=$FORCE ' ' clean=$CLEAN ' ' |
51 echo force=$FORCE ' ' clean=$CLEAN ' ' |
52 echo Compiler=$ML_SYSTEM |
52 echo Compiler=$ML_SYSTEM |
53 echo Running on `hostname` |
53 echo Running on `hostname` |
54 echo Log files will be called make$$.log.gz |
54 echo Log files will be called make$$.log.gz |
55 case $TEST in |
55 case $TEST in |
56 test) echo; echo ' **** Full test: WILL TAKE MANY HOURS ****' |
56 test) echo; echo ' **** Full test: WILL TAKE MANY HOURS ****' |
57 echo ' **** Consider the -notest switch ****' |
57 echo ' **** Consider the -notest switch ****' |
58 esac |
58 esac |
59 |
59 |
60 mkdir -p $ISABELLE_OUTPUT_DIR |
60 mkdir -p $ISABELLE_OUTPUT |
61 |
61 |
62 case $FORCE.$EXEC in |
62 case $FORCE.$EXEC in |
63 on.on) (cd $ISABELLE_OUTPUT_DIR; |
63 on.on) (cd $ISABELLE_OUTPUT; |
64 for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP |
64 for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP |
65 do |
65 do |
66 rm -f $f |
66 rm -f $f |
67 done) |
67 done) |
68 esac |
68 esac |
89 echo '*****Set theory (ZF)*****' |
89 echo '*****Set theory (ZF)*****' |
90 (cd ZF; $ISATOOL make $NO $TEST > make$$.log) |
90 (cd ZF; $ISATOOL make $NO $TEST > make$$.log) |
91 tail ZF/make$$.log |
91 tail ZF/make$$.log |
92 gzip ZF/make$$.log |
92 gzip ZF/make$$.log |
93 case $CLEAN.$EXEC in |
93 case $CLEAN.$EXEC in |
94 on.on) rm -f $ISABELLE_OUTPUT_DIR/ZF |
94 on.on) rm -f $ISABELLE_OUTPUT/ZF |
95 esac |
95 esac |
96 |
96 |
97 echo |
97 echo |
98 echo |
98 echo |
99 echo '*****Classical Computational Logic (CCL)*****' |
99 echo '*****Classical Computational Logic (CCL)*****' |
100 (cd CCL; $ISATOOL make $NO $TEST > make$$.log) |
100 (cd CCL; $ISATOOL make $NO $TEST > make$$.log) |
101 tail CCL/make$$.log |
101 tail CCL/make$$.log |
102 gzip CCL/make$$.log |
102 gzip CCL/make$$.log |
103 case $CLEAN.$EXEC in |
103 case $CLEAN.$EXEC in |
104 on.on) rm -f $ISABELLE_OUTPUT_DIR/CCL |
104 on.on) rm -f $ISABELLE_OUTPUT/CCL |
105 esac |
105 esac |
106 |
106 |
107 echo |
107 echo |
108 echo |
108 echo |
109 echo '*****Domain Theory (LCF)*****' |
109 echo '*****Domain Theory (LCF)*****' |
110 (cd LCF; $ISATOOL make $NO $TEST > make$$.log) |
110 (cd LCF; $ISATOOL make $NO $TEST > make$$.log) |
111 tail LCF/make$$.log |
111 tail LCF/make$$.log |
112 gzip LCF/make$$.log |
112 gzip LCF/make$$.log |
113 case $CLEAN.$EXEC in |
113 case $CLEAN.$EXEC in |
114 on.on) rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF |
114 on.on) rm -f $ISABELLE_OUTPUT/FOL $ISABELLE_OUTPUT/LCF |
115 esac |
115 esac |
116 |
116 |
117 echo |
117 echo |
118 echo |
118 echo |
119 echo '*****Constructive Type Theory (CTT)*****' |
119 echo '*****Constructive Type Theory (CTT)*****' |
120 (cd CTT; $ISATOOL make $NO $TEST > make$$.log) |
120 (cd CTT; $ISATOOL make $NO $TEST > make$$.log) |
121 tail CTT/make$$.log |
121 tail CTT/make$$.log |
122 gzip CTT/make$$.log |
122 gzip CTT/make$$.log |
123 case $CLEAN.$EXEC in |
123 case $CLEAN.$EXEC in |
124 on.on) rm -f $ISABELLE_OUTPUT_DIR/CTT |
124 on.on) rm -f $ISABELLE_OUTPUT/CTT |
125 esac |
125 esac |
126 |
126 |
127 echo |
127 echo |
128 echo |
128 echo |
129 echo '*****Sequent Calculi (Sequents)*****' |
129 echo '*****Sequent Calculi (Sequents)*****' |
130 (cd Sequents; $ISATOOL make $NO $TEST > make$$.log) |
130 (cd Sequents; $ISATOOL make $NO $TEST > make$$.log) |
131 tail Sequents/make$$.log |
131 tail Sequents/make$$.log |
132 gzip Sequents/make$$.log |
132 gzip Sequents/make$$.log |
133 case $CLEAN.$EXEC in |
133 case $CLEAN.$EXEC in |
134 on.on) rm -f $ISABELLE_OUTPUT_DIR/Sequents |
134 on.on) rm -f $ISABELLE_OUTPUT/Sequents |
135 esac |
135 esac |
136 |
136 |
137 echo |
137 echo |
138 echo |
138 echo |
139 echo '*****Higher-Order Logic (HOL)*****' |
139 echo '*****Higher-Order Logic (HOL)*****' |
147 echo '*****LCF in HOL (HOLCF)*****' |
147 echo '*****LCF in HOL (HOLCF)*****' |
148 (cd HOLCF; $ISATOOL make $NO $TEST > make$$.log) |
148 (cd HOLCF; $ISATOOL make $NO $TEST > make$$.log) |
149 tail HOLCF/make$$.log |
149 tail HOLCF/make$$.log |
150 gzip HOLCF/make$$.log |
150 gzip HOLCF/make$$.log |
151 case $CLEAN.$EXEC in |
151 case $CLEAN.$EXEC in |
152 on.on) rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF |
152 on.on) rm -f $ISABELLE_OUTPUT/HOL $ISABELLE_OUTPUT/HOLCF |
153 esac |
153 esac |
154 |
154 |
155 echo |
155 echo |
156 echo |
156 echo |
157 echo '*****The Lambda-Cube (Cube)*****' |
157 echo '*****The Lambda-Cube (Cube)*****' |
158 (cd Cube; $ISATOOL make $NO $TEST > make$$.log) |
158 (cd Cube; $ISATOOL make $NO $TEST > make$$.log) |
159 case $CLEAN.$EXEC in |
159 case $CLEAN.$EXEC in |
160 on.on) rm -f $ISABELLE_OUTPUT_DIR/Cube |
160 on.on) rm -f $ISABELLE_OUTPUT/Cube |
161 esac |
161 esac |
162 tail Cube/make$$.log |
162 tail Cube/make$$.log |
163 gzip Cube/make$$.log |
163 gzip Cube/make$$.log |
164 |
164 |
165 echo |
165 echo |
166 echo |
166 echo |
167 echo '*****First-Order Logic with Proof Terms (FOLP)*****' |
167 echo '*****First-Order Logic with Proof Terms (FOLP)*****' |
168 (cd FOLP; $ISATOOL make $NO $TEST > make$$.log) |
168 (cd FOLP; $ISATOOL make $NO $TEST > make$$.log) |
169 case $CLEAN.$EXEC in |
169 case $CLEAN.$EXEC in |
170 on.on) rm -f $ISABELLE_OUTPUT_DIR/FOLP |
170 on.on) rm -f $ISABELLE_OUTPUT/FOLP |
171 esac |
171 esac |
172 tail FOLP/make$$.log |
172 tail FOLP/make$$.log |
173 gzip FOLP/make$$.log |
173 gzip FOLP/make$$.log |
174 |
174 |
175 case $TEST.$EXEC in |
175 case $TEST.$EXEC in |