author  wenzelm 
Sun, 20 Jan 2013 13:59:13 +0100  
changeset 50990  11996ea98bbe 
parent 48445  cb4136e4cabf 
permissions  rwxrxrx 
10555  1 
#!/usr/bin/env bash 
2808  2 
# 
9788  3 
# Author: Markus Wenzel, TU Muenchen 
2808  4 
# 
5 
# DESCRIPTION: build objectlogic or run examples 

6 

7 

8 
## diagnostics 

9 

10511  10 
PRG="$(basename "$0")" 
2808  11 

12 
function usage() 

13 
{ 

14 
echo 

28650  15 
echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME" 
2808  16 
echo 
17 
echo " Options are:" 

17194
70d96933c210
added option C: copy existing document directory;
wenzelm
parents:
17050
diff
changeset

18 
echo " C BOOL copy existing document directory to D PATH (default true)" 
8197
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

19 
echo " D PATH dump generated document sources into PATH" 
23972  20 
echo " M MAX multithreading: maximum number of worker threads (default 1)" 
6940  21 
echo " P PATH set path for remote theory browsing information" 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

22 
echo " Q INT set threshold for subproof parallelization (default 100)" 
24118  23 
echo " T LEVEL multithreading: trace level (default 0)" 
42004  24 
echo " V VARIANT declare alternative document VARIANT" 
6212  25 
echo " b build mode (output heap image, using current dir)" 
7737  26 
echo " d FORMAT build document as FORMAT (default false)" 
15269
f856f4f3258f
isatool usedir: ML root file can now be specified (previously hardcoded as ROOT.ML)
webertj
parents:
14981
diff
changeset

27 
echo " f NAME use ML file NAME (default ROOT.ML)" 
11847  28 
echo " g BOOL generate session graph image for document (default false)" 
29 
echo " i BOOL generate HTML and graph browser information (default false)" 

10562  30 
echo " m MODE add print mode for output" 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

31 
echo " p LEVEL set level of detail for proof objects (default 0)" 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

32 
echo " q LEVEL set level of parallel proof checking (default 1)" 
6212  33 
echo " r reset session path" 
2808  34 
echo " s NAME override session NAME" 
31688  35 
echo " t BOOL internal session timing (default false)" 
11577  36 
echo " v BOOL be verbose (default false)" 
2808  37 
echo 
38 
echo " Build objectlogic or run examples. Also creates browsing" 

39 
echo " information (HTML etc.) according to settings." 

40 
echo 

7461  41 
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" 
42 
echo 

29089  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 

2808  48 
exit 1 
49 
} 

50 

11577  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 
{ 

12912  64 
[ n "$1" a z "$(echo "$1"  tr d '[09]')" ]  fail "Bad number: \"$1\"" 
11577  65 
} 
66 

2808  67 

68 
## process command line 

69 

70 
# options 

71 

24061  72 
COPY_DUMP=true 
8197
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

73 
DUMP="" 
23972  74 
MAXTHREADS="1" 
8197
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

75 
RPATH="" 
24118  76 
TRACETHREADS="0" 
42004  77 
DOCUMENT_VARIANTS="" 
2808  78 
BUILD="" 
7737  79 
DOCUMENT=false 
17050  80 
ROOT_FILE="ROOT.ML" 
11847  81 
DOCUMENT_GRAPH=false 
3747
cd9b6c86926c
There is now one single option i for generating theory browsing
berghofe
parents:
3636
diff
changeset

82 
INFO=false 
10562  83 
MODES="" 
6212  84 
RESET=false 
2808  85 
SESSION="" 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

86 
PROOFS="0" 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

87 
PARALLEL_PROOFS="1" 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

88 
PARALLEL_PROOFS_THRESHOLD="100" 
31688  89 
TIMING=false 
11577  90 
VERBOSE=false 
2808  91 

2917  92 
function getoptions() 
93 
{ 

94 
OPTIND=1 

41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

95 
while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT 
2917  96 
do 
97 
case "$OPT" in 

17194
70d96933c210
added option C: copy existing document directory;
wenzelm
parents:
17050
diff
changeset

98 
C) 
70d96933c210
added option C: copy existing document directory;
wenzelm
parents:
17050
diff
changeset

99 
check_bool "$OPTARG" 
70d96933c210
added option C: copy existing document directory;
wenzelm
parents:
17050
diff
changeset

100 
COPY_DUMP="$OPTARG" 
70d96933c210
added option C: copy existing document directory;
wenzelm
parents:
17050
diff
changeset

101 
;; 
8197
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

102 
D) 
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

103 
DUMP="$OPTARG" 
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

104 
;; 
23972  105 
M) 
25774  106 
if [ "$OPTARG" = max ]; then 
29435
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option Q), which can be disabled in lowmemory situations;
wenzelm
parents:
29143
diff
changeset

107 
MAXTHREADS=0 
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option Q), which can be disabled in lowmemory situations;
wenzelm
parents:
29143
diff
changeset

108 
else 
25774  109 
check_number "$OPTARG" 
110 
MAXTHREADS="$OPTARG" 

29435
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option Q), which can be disabled in lowmemory situations;
wenzelm
parents:
29143
diff
changeset

111 
fi 
23972  112 
;; 
8197
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

113 
P) 
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

114 
RPATH="$OPTARG" 
baab8e487fad
D PATH: dump generated document sources into PATH;
wenzelm
parents:
7888
diff
changeset

115 
;; 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

116 
Q) 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

117 
check_number "$OPTARG" 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

118 
PARALLEL_PROOFS_THRESHOLD="$OPTARG" 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
34261
diff
changeset

119 
;; 
24061  120 
T) 
24118  121 
check_number "$OPTARG" 
24061  122 
TRACETHREADS="$OPTARG" 
123 
;; 

17050  124 
V) 
42004  125 
if [ z "$DOCUMENT_VARIANTS" ]; then 
126 
DOCUMENT_VARIANTS="\"$OPTARG\"" 

17050  127 
else 
42004  128 
DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\"" 
17050  129 
fi 
130 
;; 

2917  131 
b) 
132 
BUILD=true 

133 
;; 

7737  134 
d) 
135 
DOCUMENT="$OPTARG" 

136 
;; 

15269
f856f4f3258f
isatool usedir: ML root file can now be specified (previously hardcoded as ROOT.ML)
webertj
parents:
14981
diff
changeset

137 
f) 
f856f4f3258f
isatool usedir: ML root file can now be specified (previously hardcoded as ROOT.ML)
webertj
parents:
14981
diff
changeset

138 
ROOT_FILE="$OPTARG" 
f856f4f3258f
isatool usedir: ML root file can now be specified (previously hardcoded as ROOT.ML)
webertj
parents:
14981
diff
changeset

139 
;; 
11847  140 
g) 
141 
check_bool "$OPTARG" 

142 
DOCUMENT_GRAPH="$OPTARG" 

143 
;; 

3747
cd9b6c86926c
There is now one single option i for generating theory browsing
berghofe
parents:
3636
diff
changeset

144 
i) 
11577  145 
check_bool "$OPTARG" 
3747
cd9b6c86926c
There is now one single option i for generating theory browsing
berghofe
parents:
3636
diff
changeset

146 
INFO="$OPTARG" 
2917  147 
;; 
10562  148 
m) 
149 
if [ z "$MODES" ]; then 

150 
MODES="\"$OPTARG\"" 

151 
else 

10585  152 
MODES="\"$OPTARG\", $MODES" 
10562  153 
fi 
154 
;; 

11535
7f4c5cdea239
Added new option for setting level of detail for proof objects.
berghofe
parents:
10585
diff
changeset

155 
p) 
11577  156 
check_number "$OPTARG" 
11543
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11535
diff
changeset

157 
PROOFS="$OPTARG" 
11535
7f4c5cdea239
Added new option for setting level of detail for proof objects.
berghofe
parents:
10585
diff
changeset

158 
;; 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

159 
q) 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

160 
check_number "$OPTARG" 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

161 
PARALLEL_PROOFS="$OPTARG" 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset

162 
;; 
6212  163 
r) 
164 
RESET=true 

165 
;; 

2917  166 
s) 
167 
SESSION="$OPTARG" 

168 
;; 

31688  169 
t) 
170 
check_bool "$OPTARG" 

171 
TIMING="$OPTARG" 

172 
;; 

11577  173 
v) 
174 
check_bool "$OPTARG" 

175 
VERBOSE="$OPTARG" 

176 
;; 

2917  177 
\?) 
178 
usage 

179 
;; 

180 
esac 

181 
done 

182 
} 

2808  183 

31307
7015fee8c3e8
ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");
wenzelm
parents:
29435
diff
changeset

184 
eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)" 
7015fee8c3e8
ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");
wenzelm
parents:
29435
diff
changeset

185 
getoptions "${OPTIONS[@]}" 
2917  186 

187 
getoptions "$@" 

2808  188 
shift $(($OPTIND  1)) 
189 

190 

191 
# args 

192 

9788  193 
[ "$#" ne 2 ] && usage 
2808  194 

195 
LOGIC="$1"; shift 

196 
NAME="$1"; shift 

197 

9788  198 
[ z "$SESSION" ] && SESSION=$(basename "$NAME") 
2808  199 

4419  200 

201 

202 
## main 

3636
3f2e55e5bacc
Added some code for generating theory browsing data.
berghofe
parents:
3504
diff
changeset

203 

4451  204 
# prepare browser info dir 
4419  205 

25235  206 
if [ "$INFO" = "true" a ! f "$ISABELLE_BROWSER_INFO/index.html" ]; then 
9788  207 
mkdir p "$ISABELLE_BROWSER_INFO" 
208 
cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif" 

25234  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" 

3636
3f2e55e5bacc
Added some code for generating theory browsing data.
berghofe
parents:
3504
diff
changeset

212 
fi 
3f2e55e5bacc
Added some code for generating theory browsing data.
berghofe
parents:
3504
diff
changeset

213 

2808  214 

4451  215 
# prepare log dir 
216 

217 
LOGDIR="$ISABELLE_OUTPUT/log" 

218 
mkdir p "$LOGDIR" 

219 

220 

221 
# run isabelle 

222 

7737  223 
PARENT=$(basename "$LOGIC") 
224 

11949  225 
if [ z "$BUILD" ]; then 
226 
cd "$NAME"  fail "Bad session directory '$NAME'" 

227 
fi 

4451  228 

11847  229 
if [ "$DOCUMENT" != false ]; then 
8568  230 
DOC="$DOCUMENT" 
231 
else 

232 
DOC="" 

233 
fi 

7737  234 

235 

18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestartstop.bash;
wenzelm
parents:
17194
diff
changeset

236 
. "$ISABELLE_HOME/lib/scripts/timestart.bash" 
6249  237 

2808  238 
if [ n "$BUILD" ]; then 
4451  239 
ITEM="$SESSION" 
11577  240 
echo "Building $ITEM ..." >&2 
4451  241 
LOG="$LOGDIR/$ITEM" 
242 

28502  243 
"$ISABELLE_PROCESS" \ 
48445  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;" \ 
31317
1f5740424c69
removed "compress" option from isabelleprocess and isabelle usedir  this is always enabled;
wenzelm
parents:
31307
diff
changeset

245 
q w $LOGIC $NAME > "$LOG" 
9788  246 
RC="$?" 
2808  247 
else 
9788  248 
ITEM=$(basename "$LOGIC")"$SESSION" 
11577  249 
echo "Running $ITEM ..." >&2 
4451  250 
LOG="$LOGDIR/$ITEM" 
251 

28502  252 
"$ISABELLE_PROCESS" \ 
48445  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();" \ 
11577  254 
r q "$LOGIC" > "$LOG" 
9788  255 
RC="$?" 
6212  256 
cd .. 
2808  257 
fi 
4451  258 

18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestartstop.bash;
wenzelm
parents:
17194
diff
changeset

259 
. "$ISABELLE_HOME/lib/scripts/timestop.bash" 
4451  260 

261 

262 
# exit status 

263 

9788  264 
if [ "$RC" eq 0 ]; then 
18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestartstop.bash;
wenzelm
parents:
17194
diff
changeset

265 
echo "Finished $ITEM ($TIMES_REPORT)" >&2 
4451  266 
gzip force "$LOG" 
267 
else 

11577  268 
{ echo "$ITEM FAILED"; 
269 
echo "(see also $LOG)"; 

34261
8e36b3ac6083
slightly shorter tail (again)  theory loader produces less warning spam (cf. 2524c1bbd087);
wenzelm
parents:
34238
diff
changeset

270 
echo; tail 20 "$LOG"; echo; } >&2 
4451  271 
fi 
272 

9788  273 
exit "$RC" 