--- a/bin/isabelle-process Sun Apr 06 16:36:28 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-#!/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"