1 #!/usr/bin/env bash |
|
2 # :mode=shellscript: |
|
3 # |
|
4 # Author: Makarius |
|
5 # |
|
6 # Startup script for Poly/ML 5.6. |
|
7 |
|
8 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE |
|
9 |
|
10 |
|
11 ## diagnostics |
|
12 |
|
13 function fail() |
|
14 { |
|
15 echo "$1" >&2 |
|
16 exit 2 |
|
17 } |
|
18 |
|
19 function fail_out() |
|
20 { |
|
21 fail "Unable to create output heap file: \"$OUTFILE\"" |
|
22 } |
|
23 |
|
24 function check_file() |
|
25 { |
|
26 [ ! -f "$1" ] && fail "Unable to locate \"$1\"" |
|
27 } |
|
28 |
|
29 |
|
30 ## compiler executables and libraries |
|
31 |
|
32 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)" |
|
33 |
|
34 POLY="$ML_HOME/poly" |
|
35 check_file "$POLY" |
|
36 |
|
37 librarypath "$ML_HOME" |
|
38 |
|
39 |
|
40 |
|
41 ## prepare databases |
|
42 |
|
43 case "$ML_PLATFORM" in |
|
44 *-windows) |
|
45 PLATFORM_INFILE="$(platform_path -m "$INFILE")" |
|
46 PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")" |
|
47 ;; |
|
48 *) |
|
49 PLATFORM_INFILE="$INFILE" |
|
50 PLATFORM_OUTFILE="$OUTFILE" |
|
51 ;; |
|
52 esac |
|
53 |
|
54 if [ -z "$INFILE" ]; then |
|
55 INIT="" |
|
56 case "$ML_PLATFORM" in |
|
57 *-windows) |
|
58 EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));" |
|
59 ;; |
|
60 *) |
|
61 EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
|
62 ;; |
|
63 esac |
|
64 else |
|
65 check_file "$INFILE" |
|
66 INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));" |
|
67 EXIT="" |
|
68 fi |
|
69 |
|
70 if [ -z "$OUTFILE" ]; then |
|
71 MLEXIT="" |
|
72 else |
|
73 if [ -z "$INFILE" ]; then |
|
74 MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);" |
|
75 else |
|
76 MLEXIT="Session.save \"$OUTFILE\";" |
|
77 fi |
|
78 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
79 fi |
|
80 |
|
81 |
|
82 ## run it! |
|
83 |
|
84 MLTEXT="$INIT $EXIT $MLTEXT" |
|
85 |
|
86 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then |
|
87 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ |
|
88 --error-exit </dev/null |
|
89 RC="$?" |
|
90 else |
|
91 if [ -z "$TERMINATE" ]; then |
|
92 FEEDER_OPTS="" |
|
93 else |
|
94 FEEDER_OPTS="-q" |
|
95 ML_OPTIONS="$ML_OPTIONS --error-exit" |
|
96 fi |
|
97 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
98 { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
|
99 RC="$?" |
|
100 fi |
|
101 |
|
102 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
103 |
|
104 exit "$RC" |
|
105 |
|
106 #:wrap=soft:maxLineLen=100: |
|