4 # Author: Markus Wenzel, TU Muenchen
6 # Isabelle process startup script.
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
10 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
16 PRG="$(basename "$0")"
18 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
19 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
27 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
30 echo " -C tell ML system to copy output image"
31 echo " -I startup Isar interaction mode"
32 echo " -P startup Proof General interaction mode"
33 echo " -S secure mode -- disallow critical operations"
34 echo " -X startup PGIP interaction mode"
35 echo " -W startup process wrapper (interaction via external program)"
36 echo " -c tell ML system to compress output image"
37 echo " -e MLTEXT pass MLTEXT to the ML session"
38 echo " -f pass 'Session.finish();' to the ML session"
39 echo " -m MODE add print mode for output"
40 echo " -q non-interactive session"
41 echo " -r open heap file read-only"
42 echo " -u pass 'use\"ROOT.ML\";' to the ML session"
43 echo " -w reset write permissions on OUTPUT"
45 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
46 echo " These are either names to be searched in the Isabelle path, or"
47 echo " actual file names (containing at least one /)."
48 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
60 ## process command line
77 while getopts "CIPSWXce:fm:qruw" OPT
102 MLTEXT="$MLTEXT $OPTARG"
105 MLTEXT="$MLTEXT Session.finish();"
108 if [ -z "$MODES" ]; then
111 MODES="\"$OPTARG\", $MODES"
121 MLTEXT="$MLTEXT use\"ROOT.ML\";"
132 shift $(($OPTIND - 1))
140 if [ "$#" -ge 1 ]; then
145 if [ "$#" -ge 1 ]; then
150 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
155 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
160 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
167 INFILE="$INPUT$ML_SUFFIX"
168 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
176 for DIR in $ISABELLE_PATH
178 DIR="$DIR/$ML_IDENTIFIER"
179 ISA_PATH="$ISA_PATH $DIR\n"
180 [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX"
184 if [ -z "$INFILE" ]; then
185 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
186 echo -ne "$ISA_PATH" >&2
197 [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
200 OUTFILE="$OUTPUT$ML_SUFFIX"
203 mkdir -p "$ISABELLE_OUTPUT"
204 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX"
209 ## prepare tmp directory
211 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
213 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
214 mkdir -p "$ISABELLE_TMP"
219 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
225 if [ -n "$WRAPPER" ]; then
226 MLTEXT="$MLTEXT; IsabelleProcess.init();"
227 elif [ -n "$PGIP" ]; then
228 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
229 elif [ -n "$PROOFGENERAL" ]; then
230 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
231 elif [ "$ISAR" = true ]; then
232 MLTEXT="$MLTEXT; Isar.main();"
235 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
236 ISABELLE_PID ISABELLE_TMP
238 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
239 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
241 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
245 rmdir "$ISABELLE_TMP"