bin/isabelle_process

+#!/usr/bin/env bash
+#
+# Author: Markus Wenzel, TU Muenchen
+#
+# Isabelle process startup script.
+
+if [ -L "$0" ]; then
+  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+fi
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+
+## diagnostics
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+  echo
+  echo "  Options are:"
+  echo "    -I           startup Isar interaction mode"
+  echo "    -P           startup Proof General interaction mode"
+  echo "    -S           secure mode -- disallow critical operations"
+  echo "    -T ADDR      startup process wrapper, with socket address"
+  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
+  echo "    -e MLTEXT    pass MLTEXT to the ML session"
+  echo "    -m MODE      add print mode for output"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
+  echo "    -q           non-interactive session"
+  echo "    -r           open heap file read-only"
+  echo "    -w           reset write permissions on OUTPUT"
+  echo
+  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
+  echo "  These are either names to be searched in the Isabelle path, or"
+  echo "  actual file names (containing at least one /)."
+  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+ISAR=""
+PROOFGENERAL=""
+SECURE=""
+WRAPPER_SOCKET=""
+WRAPPER_FIFOS=""
+MLTEXT=""
+MODES=""
+declare -a SYSTEM_OPTIONS=()
+TERMINATE=""
+READONLY=""
+NOWRITE=""
+
+while getopts "IPST:W:e:m:o:qrw" OPT
+do
+  case "$OPT" in
+    I)
+      ISAR=true
+      ;;
+    P)
+      PROOFGENERAL=true
+      ;;
+    S)
+      SECURE=true
+      ;;
+    T)
+      WRAPPER_SOCKET="$OPTARG"
+      ;;
+    W)
+      WRAPPER_FIFOS="$OPTARG"
+      ;;
+    e)
+      MLTEXT="$MLTEXT $OPTARG"
+      ;;
+    m)
+      if [ -z "$MODES" ]; then
+        MODES="\"$OPTARG\""
+      else
+        MODES="\"$OPTARG\", $MODES"
+      fi
+      ;;
+    o)
+      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
+      ;;
+    q)
+      TERMINATE=true
+      ;;
+    r)
+      READONLY=true
+      ;;
+    w)
+      NOWRITE=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+INPUT=""
+OUTPUT=""
+
+if [ "$#" -ge 1 ]; then
+  INPUT="$1"
+  shift
+fi
+
+if [ "$#" -ge 1 ]; then
+  OUTPUT="$1"
+  shift
+fi
+
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+## check ML system
+
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
+
+
+## input heap file
+
+[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+
+case "$INPUT" in
+  RAW_ML_SYSTEM)
+    INFILE=""
+    ;;
+  */*)
+    INFILE="$INPUT"
+    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
+    ;;
+  *)
+    INFILE=""
+    ISA_PATH=""
+
+    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
+    for DIR in "${PATHS[@]}"
+    do
+      DIR="$DIR/$ML_IDENTIFIER"
+      ISA_PATH="$ISA_PATH  $DIR\n"
+      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+    done
+
+    if [ -z "$INFILE" ]; then
+      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
+      echo -ne "$ISA_PATH" >&2
+      exit 2
+    fi
+    ;;
+esac
+
+
+## output heap file
+
+case "$OUTPUT" in
+  "")
+    if [ -z "$READONLY" -a -w "$INFILE" ]; then
+      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+    fi
+    ;;
+  */*)
+    OUTFILE="$OUTPUT"
+    ;;
+  *)
+    mkdir -p "$ISABELLE_OUTPUT"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
+    ;;
+esac
+
+
+## prepare tmp directory
+
+[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+ISABELLE_PID="$$"
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
+mkdir -p "$ISABELLE_TMP"
+
+
+## run it!
+
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+
+[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
+
+[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
+
+NICE="nice"
+
+if [ -n "$WRAPPER_SOCKET" ]; then
+  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
+elif [ -n "$WRAPPER_FIFOS" ]; then
+  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
+  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
+  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
+  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
+  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
+else
+  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
+  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+    fail "Failed to retrieve Isabelle system options"
+  if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
+    MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
+  fi
+  if [ -n "$PROOFGENERAL" ]; then
+    MLTEXT="$MLTEXT; ProofGeneral.init ();"
+  elif [ -n "$ISAR" ]; then
+    MLTEXT="$MLTEXT; Isar.main ();"
+  else
+    NICE=""
+  fi
+fi
+
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
+
+if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
+  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+else
+  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+fi
+RC="$?"
+
+[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
+rmdir "$ISABELLE_TMP"
+
+exit "$RC"