author | nipkow |
Tue, 18 Sep 2012 03:33:53 +0200 | |
changeset 49433 | 1095f240146a |
parent 48662 | b171bcd5dd86 |
child 51099 | 2ef891f99d2c |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
2301 | 2 |
# |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
3 |
# Author: Makarius |
2314 | 4 |
# |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
5 |
# Poly/ML 5.1/5.2 startup script. |
9977 | 6 |
|
31317
1f5740424c69
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents:
31315
diff
changeset
|
7 |
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE |
2301 | 8 |
|
9 |
||
10 |
## diagnostics |
|
11 |
||
40544 | 12 |
function fail() |
13 |
{ |
|
14 |
echo "$1" >&2 |
|
15 |
exit 2 |
|
16 |
} |
|
17 |
||
2349 | 18 |
function fail_out() |
2301 | 19 |
{ |
40544 | 20 |
fail "Unable to create output heap file: \"$OUTFILE\"" |
2301 | 21 |
} |
22 |
||
10206 | 23 |
function check_file() |
5063 | 24 |
{ |
40544 | 25 |
[ ! -f "$1" ] && fail "Unable to locate \"$1\"" |
5063 | 26 |
} |
27 |
||
2301 | 28 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
29 |
## compiler executables and libraries |
16374 | 30 |
|
40544 | 31 |
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)" |
32 |
||
21356 | 33 |
POLY="$ML_HOME/poly" |
10206 | 34 |
check_file "$POLY" |
2301 | 35 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
36 |
if [ "$(basename "$ML_HOME")" = bin ]; then |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
37 |
POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)" |
16392 | 38 |
else |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
39 |
POLYLIB="$ML_HOME" |
16392 | 40 |
fi |
10206 | 41 |
|
41614
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
40544
diff
changeset
|
42 |
librarypath "$POLYLIB" |
9765 | 43 |
|
44 |
||
2301 | 45 |
## prepare databases |
46 |
||
47 |
if [ -z "$INFILE" ]; then |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
48 |
INIT="" |
48662 | 49 |
EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" |
10105 | 50 |
else |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
51 |
check_file "$INFILE" |
48662 | 52 |
INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));" |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
53 |
EXIT="" |
2301 | 54 |
fi |
55 |
||
56 |
if [ -z "$OUTFILE" ]; then |
|
39619 | 57 |
COMMIT='fun commit () = false;' |
58 |
MLEXIT="" |
|
2301 | 59 |
else |
31317
1f5740424c69
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents:
31315
diff
changeset
|
60 |
COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
61 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
39619 | 62 |
MLEXIT="commit();" |
2301 | 63 |
fi |
64 |
||
65 |
||
66 |
## run it! |
|
67 |
||
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
68 |
MLTEXT="$INIT $EXIT $COMMIT $MLTEXT" |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
69 |
|
16254
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
70 |
if [ -z "$TERMINATE" ]; then |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
71 |
FEEDER_OPTS="" |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
72 |
else |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
73 |
FEEDER_OPTS="-q" |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
74 |
fi |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
75 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
25123
diff
changeset
|
76 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
48002
6de952f4069f
potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
wenzelm
parents:
41614
diff
changeset
|
77 |
{ read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
9789 | 78 |
RC="$?" |
2301 | 79 |
|
4505 | 80 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
2301 | 81 |
|
9789 | 82 |
exit "$RC" |
40480 | 83 |
|
84 |
#:wrap=soft:maxLineLen=100: |