author | huffman |
Fri, 20 Jun 2008 19:59:00 +0200 | |
changeset 27296 | eec7a1889ca5 |
parent 14981 | e73f8140af78 |
child 29145 | b1c6f4563df7 |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
9253
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
2 |
# |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
3 |
# $Id$ |
9789 | 4 |
# Author: Markus Wenzel, TU Muenchen |
9253
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
5 |
# |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
6 |
# Moscow ML 2.00 startup script |
9977 | 7 |
|
10105 | 8 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
9253
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
9 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
10 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
11 |
## diagnostics |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
12 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
13 |
function fail_out() |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
14 |
{ |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
16 |
exit 2 |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
17 |
} |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
18 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
19 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
20 |
## prepare databases |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
21 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
22 |
MOSML="mosml -P sml90" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
23 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
24 |
if [ -z "$INFILE" ]; then |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
25 |
EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;' |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
26 |
else |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
27 |
EXIT="" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
28 |
echo "Cannot load images yet!" >&2 |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
29 |
exit 2 |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
30 |
fi |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
31 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
32 |
if [ -z "$OUTFILE" ]; then |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
33 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
34 |
else |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
35 |
COMMIT="fun commit () = true;" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
36 |
echo "WARNING: cannot save images yet!" >&2 |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
37 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
38 |
fi |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
39 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
40 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
41 |
## run it! |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
42 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
43 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
44 |
MLEXIT="commit();" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
45 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
46 |
if [ -z "$TERMINATE" ]; then |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
47 |
FEEDER_OPTS="" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
48 |
else |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
49 |
FEEDER_OPTS="-q" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
50 |
fi |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
51 |
|
9789 | 52 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
9794 | 53 |
{ read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
9789 | 54 |
RC="$?" |
9253
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
55 |
|
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
56 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
fafb8dfab7f6
run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff
changeset
|
57 |
|
9789 | 58 |
exit "$RC" |