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 " -I startup Isar interaction mode"
30 echo " -P startup Proof General interaction mode"
31 echo " -S secure mode -- disallow critical operations"
32 echo " -T ADDR startup process wrapper, with socket address"
33 echo " -W IN:OUT startup process wrapper, with input/output fifos"
34 echo " -X startup PGIP interaction mode"
35 echo " -e MLTEXT pass MLTEXT to the ML session"
36 echo " -f pass 'Session.finish();' to the ML session"
37 echo " -m MODE add print mode for output"
38 echo " -q non-interactive session"
39 echo " -r open heap file read-only"
40 echo " -u pass 'use\"ROOT.ML\";' to the ML session"
41 echo " -w reset write permissions on OUTPUT"
43 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
44 echo " These are either names to be searched in the Isabelle path, or"
45 echo " actual file names (containing at least one /)."
46 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
58 ## process command line
74 while getopts "IPST:W:Xe:fm:qruw" OPT
87 WRAPPER_SOCKET="$OPTARG"
90 WRAPPER_FIFOS="$OPTARG"
96 MLTEXT="$MLTEXT $OPTARG"
99 MLTEXT="$MLTEXT Session.finish();"
102 if [ -z "$MODES" ]; then
105 MODES="\"$OPTARG\", $MODES"
115 MLTEXT="$MLTEXT use\"ROOT.ML\";"
126 shift $(($OPTIND - 1))
134 if [ "$#" -ge 1 ]; then
139 if [ "$#" -ge 1 ]; then
144 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
149 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
154 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
162 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
168 splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
169 for DIR in "${PATHS[@]}"
171 DIR="$DIR/$ML_IDENTIFIER"
172 ISA_PATH="$ISA_PATH $DIR\n"
173 [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
176 if [ -z "$INFILE" ]; then
177 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
178 echo -ne "$ISA_PATH" >&2
189 if [ -z "$READONLY" -a -w "$INFILE" ]; then
190 perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
197 mkdir -p "$ISABELLE_OUTPUT"
198 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
203 ## prepare tmp directory
205 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
207 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
208 mkdir -p "$ISABELLE_TMP"
213 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
215 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
217 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
221 if [ -n "$WRAPPER_SOCKET" ]; then
222 MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
223 elif [ -n "$WRAPPER_FIFOS" ]; then
224 splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
225 [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
226 [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
227 [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
228 MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
229 elif [ -n "$PGIP" ]; then
230 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
231 elif [ -n "$PROOFGENERAL" ]; then
232 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
233 elif [ "$ISAR" = true ]; then
234 if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
235 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
236 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
238 MLTEXT="$MLTEXT; Isar.main ();"
243 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
245 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
246 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
248 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
252 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
253 rmdir "$ISABELLE_TMP"