author | wenzelm |
Thu, 03 Mar 2016 21:35:16 +0100 | |
changeset 62507 | 15c36c181130 |
parent 62506 | 860cd901ab43 |
child 62542 | b27b7c2200b9 |
permissions | -rwxr-xr-x |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
2 |
# |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
3 |
# Author: Makarius |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
4 |
# |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
5 |
# Isabelle process startup script. |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
6 |
|
15843 | 7 |
if [ -L "$0" ]; then |
8 |
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
|
15967 | 9 |
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
15843 | 10 |
fi |
11 |
||
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
12 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
13 |
## settings |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
14 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
15 |
PRG="$(basename "$0")" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
16 |
|
15967 | 17 |
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
18 |
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
19 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
20 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
21 |
## diagnostics |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
22 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
23 |
function usage() |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
24 |
{ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
25 |
echo |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
26 |
echo "Usage: $PRG [OPTIONS] [HEAP]" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
27 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
28 |
echo " Options are:" |
57581
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
29 |
echo " -O system options from given YXML file" |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
30 |
echo " -P SOCKET startup process wrapper via TCP socket" |
20929 | 31 |
echo " -S secure mode -- disallow critical operations" |
62506 | 32 |
echo " -e ML_EXPR evaluate ML expression on startup" |
33 |
echo " -f ML_FILE evaluate ML file on startup" |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
34 |
echo " -m MODE add print mode for output" |
52056 | 35 |
echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
36 |
echo " -q non-interactive session" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
37 |
echo |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
38 |
echo " If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;" |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
39 |
echo " if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM," |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
40 |
echo " the initial ML heap is used." |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
41 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
42 |
exit 1 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
43 |
} |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
44 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
45 |
function fail() |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
46 |
{ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
47 |
echo "$1" >&2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
48 |
exit 2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
49 |
} |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
50 |
|
62506 | 51 |
function check_file() |
52 |
{ |
|
53 |
[ ! -f "$1" ] && fail "Bad file: \"$1\"" |
|
54 |
} |
|
55 |
||
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
56 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
57 |
## process command line |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
58 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
59 |
# options |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
60 |
|
57581
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
61 |
OPTIONS_FILE="" |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
62 |
PROCESS_SOCKET="" |
20923 | 63 |
SECURE="" |
62506 | 64 |
declare -a LAST_ML_OPTIONS=() |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
65 |
MODES="" |
52056 | 66 |
declare -a SYSTEM_OPTIONS=() |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
67 |
TERMINATE="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
68 |
|
62506 | 69 |
while getopts "O:P:Se:f:m:o:q" OPT |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
70 |
do |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
71 |
case "$OPT" in |
57581
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
72 |
O) |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
73 |
OPTIONS_FILE="$OPTARG" |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
74 |
;; |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
75 |
P) |
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
76 |
PROCESS_SOCKET="$OPTARG" |
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
77 |
;; |
20923 | 78 |
S) |
79 |
SECURE=true |
|
80 |
;; |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
81 |
e) |
62506 | 82 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" |
83 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG" |
|
84 |
;; |
|
85 |
f) |
|
86 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use" |
|
87 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG" |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
88 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
89 |
m) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
90 |
if [ -z "$MODES" ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
91 |
MODES="\"$OPTARG\"" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
92 |
else |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
93 |
MODES="\"$OPTARG\", $MODES" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
94 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
95 |
;; |
52056 | 96 |
o) |
97 |
SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG" |
|
98 |
;; |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
99 |
q) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
100 |
TERMINATE=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
101 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
102 |
\?) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
103 |
usage |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
104 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
105 |
esac |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
106 |
done |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
107 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
108 |
shift $(($OPTIND - 1)) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
109 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
110 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
111 |
# args |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
112 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
113 |
HEAP="" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
114 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
115 |
if [ "$#" -ge 1 ]; then |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
116 |
HEAP="$1" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
117 |
shift |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
118 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
119 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
120 |
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
121 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
122 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
123 |
## check ML system |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
124 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
125 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
126 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
127 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
128 |
## heap file |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
129 |
|
62506 | 130 |
declare -a FIRST_ML_OPTIONS=() |
131 |
||
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
132 |
[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
133 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
134 |
case "$HEAP" in |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
135 |
RAW_ML_SYSTEM) |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
136 |
HEAP_FILE="" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
137 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
138 |
*/*) |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
139 |
HEAP_FILE="$HEAP" |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
140 |
[ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\"" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
141 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
142 |
*) |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
143 |
HEAP_FILE="" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
144 |
ISA_PATH="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
145 |
|
32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32322
diff
changeset
|
146 |
splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}") |
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
31797
diff
changeset
|
147 |
for DIR in "${PATHS[@]}" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
148 |
do |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
149 |
DIR="$DIR/$ML_IDENTIFIER" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
150 |
ISA_PATH="$ISA_PATH $DIR\n" |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
151 |
[ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
152 |
done |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
153 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
154 |
if [ -z "$HEAP_FILE" ]; then |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
155 |
echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2 |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
156 |
echo -ne "$ISA_PATH" >&2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
157 |
exit 2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
158 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
159 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
160 |
esac |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
161 |
|
62506 | 162 |
if [ -z "$HEAP_FILE" ]; then |
163 |
case "$ML_PLATFORM" in |
|
164 |
*-windows) |
|
165 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
|
166 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="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))" |
|
167 |
;; |
|
168 |
*) |
|
169 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
|
170 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)" |
|
171 |
;; |
|
172 |
esac |
|
173 |
else |
|
174 |
check_file "$HEAP_FILE" |
|
175 |
case "$ML_PLATFORM" in |
|
176 |
*-windows) |
|
177 |
PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")" |
|
178 |
;; |
|
179 |
*) |
|
180 |
PLATFORM_HEAP_FILE="$HEAP_FILE" |
|
181 |
;; |
|
182 |
esac |
|
183 |
PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")" |
|
184 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
|
62507 | 185 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)" |
62506 | 186 |
fi |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
187 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
188 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
189 |
## prepare tmp directory |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
190 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
191 |
[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
16874 | 192 |
ISABELLE_PID="$$" |
17792 | 193 |
ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
16874 | 194 |
mkdir -p "$ISABELLE_TMP" |
61319
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
59350
diff
changeset
|
195 |
chmod $(umask -S) "$ISABELLE_TMP" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
196 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
197 |
|
62506 | 198 |
## ML text |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
199 |
|
62506 | 200 |
if [ -n "$MODES" ]; then |
201 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
|
202 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Unsynchronized.change print_mode (append [$MODES])" |
|
203 |
fi |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
204 |
|
62506 | 205 |
if [ -n "$SECURE" ]; then |
206 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" |
|
207 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()" |
|
208 |
fi |
|
20923 | 209 |
|
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
210 |
if [ -n "$PROCESS_SOCKET" ]; then |
62506 | 211 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" |
212 |
LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\"" |
|
51948
cb5dbc9a06f9
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm
parents:
51938
diff
changeset
|
213 |
else |
51952
4517ceb545c1
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
wenzelm
parents:
51948
diff
changeset
|
214 |
ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" |
57581
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
215 |
if [ -n "$OPTIONS_FILE" ]; then |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
216 |
[ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \ |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
217 |
fail "Cannot provide options file and options on command-line" |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
218 |
mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" || |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
219 |
fail "Failed to move options file \"$OPTIONS_FILE\"" |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
220 |
else |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
221 |
"$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \ |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
222 |
fail "Failed to retrieve Isabelle system options" |
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
56628
diff
changeset
|
223 |
fi |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
61319
diff
changeset
|
224 |
if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then |
62506 | 225 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
226 |
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()" |
|
51948
cb5dbc9a06f9
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm
parents:
51938
diff
changeset
|
227 |
fi |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
228 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
229 |
|
62506 | 230 |
|
231 |
## ML process |
|
232 |
||
233 |
check_file "$ML_HOME/poly" |
|
234 |
librarypath "$ML_HOME" |
|
235 |
||
236 |
export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
237 |
|
62506 | 238 |
if [ -n "$TERMINATE" ]; then |
239 |
"$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \ |
|
240 |
"${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null |
|
241 |
RC="$?" |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
242 |
else |
62506 | 243 |
"$ISABELLE_HOME/lib/scripts/feeder" -p | \ |
244 |
{ |
|
245 |
read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" |
|
246 |
RC="$?" |
|
247 |
kill -TERM "$FPID" |
|
248 |
exit "$RC" |
|
249 |
} |
|
250 |
RC="$?" |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
251 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
252 |
|
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
45056
diff
changeset
|
253 |
[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS" |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
254 |
rmdir "$ISABELLE_TMP" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
255 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
256 |
exit "$RC" |