1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Markus Wenzel, TU Muenchen |
|
4 # |
|
5 # DESCRIPTION: build object-logic or run examples |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG="$(basename "$0")" |
|
11 |
|
12 function usage() |
|
13 { |
|
14 echo |
|
15 echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -C BOOL copy existing document directory to -D PATH (default true)" |
|
19 echo " -D PATH dump generated document sources into PATH" |
|
20 echo " -M MAX multithreading: maximum number of worker threads (default 1)" |
|
21 echo " -P PATH set path for remote theory browsing information" |
|
22 echo " -Q INT set threshold for sub-proof parallelization (default 100)" |
|
23 echo " -T LEVEL multithreading: trace level (default 0)" |
|
24 echo " -V VARIANT declare alternative document VARIANT" |
|
25 echo " -b build mode (output heap image, using current dir)" |
|
26 echo " -d FORMAT build document as FORMAT (default false)" |
|
27 echo " -f NAME use ML file NAME (default ROOT.ML)" |
|
28 echo " -g BOOL generate session graph image for document (default false)" |
|
29 echo " -i BOOL generate HTML and graph browser information (default false)" |
|
30 echo " -m MODE add print mode for output" |
|
31 echo " -p LEVEL set level of detail for proof objects (default 0)" |
|
32 echo " -q LEVEL set level of parallel proof checking (default 1)" |
|
33 echo " -r reset session path" |
|
34 echo " -s NAME override session NAME" |
|
35 echo " -t BOOL internal session timing (default false)" |
|
36 echo " -v BOOL be verbose (default false)" |
|
37 echo |
|
38 echo " Build object-logic or run examples. Also creates browsing" |
|
39 echo " information (HTML etc.) according to settings." |
|
40 echo |
|
41 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
|
42 echo |
|
43 echo " ML_PLATFORM=$ML_PLATFORM" |
|
44 echo " ML_HOME=$ML_HOME" |
|
45 echo " ML_SYSTEM=$ML_SYSTEM" |
|
46 echo " ML_OPTIONS=$ML_OPTIONS" |
|
47 echo |
|
48 exit 1 |
|
49 } |
|
50 |
|
51 function fail() |
|
52 { |
|
53 echo "$1" >&2 |
|
54 exit 2 |
|
55 } |
|
56 |
|
57 function check_bool() |
|
58 { |
|
59 [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" |
|
60 } |
|
61 |
|
62 function check_number() |
|
63 { |
|
64 [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" |
|
65 } |
|
66 |
|
67 |
|
68 ## process command line |
|
69 |
|
70 # options |
|
71 |
|
72 COPY_DUMP=true |
|
73 DUMP="" |
|
74 MAXTHREADS="1" |
|
75 RPATH="" |
|
76 TRACETHREADS="0" |
|
77 DOCUMENT_VARIANTS="" |
|
78 BUILD="" |
|
79 DOCUMENT=false |
|
80 ROOT_FILE="ROOT.ML" |
|
81 DOCUMENT_GRAPH=false |
|
82 INFO=false |
|
83 MODES="" |
|
84 RESET=false |
|
85 SESSION="" |
|
86 PROOFS="0" |
|
87 PARALLEL_PROOFS="1" |
|
88 PARALLEL_PROOFS_THRESHOLD="100" |
|
89 TIMING=false |
|
90 VERBOSE=false |
|
91 |
|
92 function getoptions() |
|
93 { |
|
94 OPTIND=1 |
|
95 while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT |
|
96 do |
|
97 case "$OPT" in |
|
98 C) |
|
99 check_bool "$OPTARG" |
|
100 COPY_DUMP="$OPTARG" |
|
101 ;; |
|
102 D) |
|
103 DUMP="$OPTARG" |
|
104 ;; |
|
105 M) |
|
106 if [ "$OPTARG" = max ]; then |
|
107 MAXTHREADS=0 |
|
108 else |
|
109 check_number "$OPTARG" |
|
110 MAXTHREADS="$OPTARG" |
|
111 fi |
|
112 ;; |
|
113 P) |
|
114 RPATH="$OPTARG" |
|
115 ;; |
|
116 Q) |
|
117 check_number "$OPTARG" |
|
118 PARALLEL_PROOFS_THRESHOLD="$OPTARG" |
|
119 ;; |
|
120 T) |
|
121 check_number "$OPTARG" |
|
122 TRACETHREADS="$OPTARG" |
|
123 ;; |
|
124 V) |
|
125 if [ -z "$DOCUMENT_VARIANTS" ]; then |
|
126 DOCUMENT_VARIANTS="\"$OPTARG\"" |
|
127 else |
|
128 DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\"" |
|
129 fi |
|
130 ;; |
|
131 b) |
|
132 BUILD=true |
|
133 ;; |
|
134 d) |
|
135 DOCUMENT="$OPTARG" |
|
136 ;; |
|
137 f) |
|
138 ROOT_FILE="$OPTARG" |
|
139 ;; |
|
140 g) |
|
141 check_bool "$OPTARG" |
|
142 DOCUMENT_GRAPH="$OPTARG" |
|
143 ;; |
|
144 i) |
|
145 check_bool "$OPTARG" |
|
146 INFO="$OPTARG" |
|
147 ;; |
|
148 m) |
|
149 if [ -z "$MODES" ]; then |
|
150 MODES="\"$OPTARG\"" |
|
151 else |
|
152 MODES="\"$OPTARG\", $MODES" |
|
153 fi |
|
154 ;; |
|
155 p) |
|
156 check_number "$OPTARG" |
|
157 PROOFS="$OPTARG" |
|
158 ;; |
|
159 q) |
|
160 check_number "$OPTARG" |
|
161 PARALLEL_PROOFS="$OPTARG" |
|
162 ;; |
|
163 r) |
|
164 RESET=true |
|
165 ;; |
|
166 s) |
|
167 SESSION="$OPTARG" |
|
168 ;; |
|
169 t) |
|
170 check_bool "$OPTARG" |
|
171 TIMING="$OPTARG" |
|
172 ;; |
|
173 v) |
|
174 check_bool "$OPTARG" |
|
175 VERBOSE="$OPTARG" |
|
176 ;; |
|
177 \?) |
|
178 usage |
|
179 ;; |
|
180 esac |
|
181 done |
|
182 } |
|
183 |
|
184 eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)" |
|
185 getoptions "${OPTIONS[@]}" |
|
186 |
|
187 getoptions "$@" |
|
188 shift $(($OPTIND - 1)) |
|
189 |
|
190 |
|
191 # args |
|
192 |
|
193 [ "$#" -ne 2 ] && usage |
|
194 |
|
195 LOGIC="$1"; shift |
|
196 NAME="$1"; shift |
|
197 |
|
198 [ -z "$SESSION" ] && SESSION=$(basename "$NAME") |
|
199 |
|
200 |
|
201 |
|
202 ## main |
|
203 |
|
204 # prepare browser info dir |
|
205 |
|
206 if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then |
|
207 mkdir -p "$ISABELLE_BROWSER_INFO" |
|
208 cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif" |
|
209 cat "$ISABELLE_HOME/lib/html/library_index_header.template" \ |
|
210 "$ISABELLE_HOME/lib/html/library_index_content.template" \ |
|
211 "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html" |
|
212 fi |
|
213 |
|
214 |
|
215 # prepare log dir |
|
216 |
|
217 LOGDIR="$ISABELLE_OUTPUT/log" |
|
218 mkdir -p "$LOGDIR" |
|
219 |
|
220 |
|
221 # run isabelle |
|
222 |
|
223 PARENT=$(basename "$LOGIC") |
|
224 |
|
225 if [ -z "$BUILD" ]; then |
|
226 cd "$NAME" || fail "Bad session directory '$NAME'" |
|
227 fi |
|
228 |
|
229 if [ "$DOCUMENT" != false ]; then |
|
230 DOC="$DOCUMENT" |
|
231 else |
|
232 DOC="" |
|
233 fi |
|
234 |
|
235 |
|
236 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
|
237 |
|
238 if [ -n "$BUILD" ]; then |
|
239 ITEM="$SESSION" |
|
240 echo "Building $ITEM ..." >&2 |
|
241 LOG="$LOGDIR/$ITEM" |
|
242 |
|
243 "$ISABELLE_PROCESS" \ |
|
244 -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \ |
|
245 -q -w $LOGIC $NAME > "$LOG" |
|
246 RC="$?" |
|
247 else |
|
248 ITEM=$(basename "$LOGIC")-"$SESSION" |
|
249 echo "Running $ITEM ..." >&2 |
|
250 LOG="$LOGDIR/$ITEM" |
|
251 |
|
252 "$ISABELLE_PROCESS" \ |
|
253 -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \ |
|
254 -r -q "$LOGIC" > "$LOG" |
|
255 RC="$?" |
|
256 cd .. |
|
257 fi |
|
258 |
|
259 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
|
260 |
|
261 |
|
262 # exit status |
|
263 |
|
264 if [ "$RC" -eq 0 ]; then |
|
265 echo "Finished $ITEM ($TIMES_REPORT)" >&2 |
|
266 gzip --force "$LOG" |
|
267 else |
|
268 { echo "$ITEM FAILED"; |
|
269 echo "(see also $LOG)"; |
|
270 echo; tail -20 "$LOG"; echo; } >&2 |
|
271 fi |
|
272 |
|
273 exit "$RC" |
|