bin/isabelle_process

isabelle_process executable no longer supports writable heap images;

#!/usr/bin/env bash
#
# Author: Makarius
#
# 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] [HEAP]"
  echo
  echo "  Options are:"
  echo "    -O           system options from given YXML file"
  echo "    -P SOCKET    startup process wrapper via TCP socket"
  echo "    -S           secure mode -- disallow critical operations"
  echo "    -e ML_TEXT   pass ML_TEXT 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
  echo "  If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;"
  echo "  if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,"
  echo "  the initial ML heap is used."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

OPTIONS_FILE=""
PROCESS_SOCKET=""
SECURE=""
ML_TEXT=""
MODES=""
declare -a SYSTEM_OPTIONS=()
TERMINATE=""

while getopts "O:P:Se:m:o:q" OPT
do
  case "$OPT" in
    O)
      OPTIONS_FILE="$OPTARG"
      ;;
    P)
      PROCESS_SOCKET="$OPTARG"
      ;;
    S)
      SECURE=true
      ;;
    e)
      ML_TEXT="$ML_TEXT $OPTARG"
      ;;
    m)
      if [ -z "$MODES" ]; then
        MODES="\"$OPTARG\""
      else
        MODES="\"$OPTARG\", $MODES"
      fi
      ;;
    o)
      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
      ;;
    q)
      TERMINATE=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

HEAP=""

if [ "$#" -ge 1 ]; then
  HEAP="$1"
  shift
fi

[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }


## check ML system

[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."


## heap file

[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"

case "$HEAP" in
  RAW_ML_SYSTEM)
    HEAP_FILE=""
    ;;
  */*)
    HEAP_FILE="$HEAP"
    [ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\""
    ;;
  *)
    HEAP_FILE=""
    ISA_PATH=""

    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
    for DIR in "${PATHS[@]}"
    do
      DIR="$DIR/$ML_IDENTIFIER"
      ISA_PATH="$ISA_PATH  $DIR\n"
      [ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP"
    done

    if [ -z "$HEAP_FILE" ]; then
      echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2
      echo -ne "$ISA_PATH" >&2
      exit 2
    fi
    ;;
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"
chmod $(umask -S) "$ISABELLE_TMP"


## run it!

ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

[ -n "$MODES" ] && ML_TEXT="Unsynchronized.change print_mode (append [$MODES]); $ML_TEXT"

[ -n "$SECURE" ] && ML_TEXT="$ML_TEXT; Secure.set_secure ();"

if [ -n "$PROCESS_SOCKET" ]; then
  ML_TEXT="$ML_TEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
else
  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
  if [ -n "$OPTIONS_FILE" ]; then
    [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
      fail "Cannot provide options file and options on command-line"
    mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
      fail "Failed to move options file \"$OPTIONS_FILE\""
  else
    "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
      fail "Failed to retrieve Isabelle system options"
  fi
  if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
    ML_TEXT="Exn.capture_exit 2 Options.load_default (); $ML_TEXT"
  fi
fi

export HEAP_FILE ML_TEXT TERMINATE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS

if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
fi
RC="$?"

[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
rmdir "$ISABELLE_TMP"

exit "$RC"