3 # Author: Markus Wenzel, TU Muenchen
5 # Isabelle process startup script.
8 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
9 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
15 PRG="$(basename "$0")"
17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
26 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
29 echo " -O system options from given YXML file"
30 echo " -P SOCKET startup process wrapper via TCP socket"
31 echo " -S secure mode -- disallow critical operations"
32 echo " -e MLTEXT pass MLTEXT to the ML session"
33 echo " -m MODE add print mode for output"
34 echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
35 echo " -q non-interactive session"
36 echo " -r open heap file read-only"
37 echo " -w reset write permissions on OUTPUT"
39 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
40 echo " These are either names to be searched in the Isabelle path, or"
41 echo " actual file names (containing at least one /)."
42 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
54 ## process command line
63 declare -a SYSTEM_OPTIONS=()
68 while getopts "O:P:Se:m:o:qrw" OPT
72 OPTIONS_FILE="$OPTARG"
75 PROCESS_SOCKET="$OPTARG"
81 MLTEXT="$MLTEXT $OPTARG"
84 if [ -z "$MODES" ]; then
87 MODES="\"$OPTARG\", $MODES"
91 SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
108 shift $(($OPTIND - 1))
116 if [ "$#" -ge 1 ]; then
121 if [ "$#" -ge 1 ]; then
126 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
131 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
136 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
144 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
150 splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
151 for DIR in "${PATHS[@]}"
153 DIR="$DIR/$ML_IDENTIFIER"
154 ISA_PATH="$ISA_PATH $DIR\n"
155 [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
158 if [ -z "$INFILE" ]; then
159 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
160 echo -ne "$ISA_PATH" >&2
171 if [ -z "$READONLY" -a -w "$INFILE" ]; then
172 perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
179 mkdir -p "$ISABELLE_OUTPUT"
180 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
185 ## prepare tmp directory
187 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
189 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
190 mkdir -p "$ISABELLE_TMP"
195 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
197 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
199 [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
201 if [ -n "$PROCESS_SOCKET" ]; then
202 MLTEXT="$MLTEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
204 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
205 if [ -n "$OPTIONS_FILE" ]; then
206 [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
207 fail "Cannot provide options file and options on command-line"
208 mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
209 fail "Failed to move options file \"$OPTIONS_FILE\""
211 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
212 fail "Failed to retrieve Isabelle system options"
214 if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
215 MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
219 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
221 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
222 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
224 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
228 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
229 rmdir "$ISABELLE_TMP"