bin/isabelle_process

clarified isabelle_process;

#!/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_EXPR   evaluate ML expression on startup"
  echo "    -f ML_FILE   evaluate ML file on startup"
  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
}

function check_file()
{
  [ ! -f "$1" ] && fail "Bad file: \"$1\""
}


## process command line

# options

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

while getopts "O:P:Se:f:m:o:q" OPT
do
  case "$OPT" in
    O)
      OPTIONS_FILE="$OPTARG"
      ;;
    P)
      PROCESS_SOCKET="$OPTARG"
      ;;
    S)
      SECURE=true
      ;;
    e)
      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
      ;;
    f)
      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use"
      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$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

declare -a FIRST_ML_OPTIONS=()

[ -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

if [ -z "$HEAP_FILE" ]; then
  case "$ML_PLATFORM" in
    *-windows)
      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
      ;;
    *)
      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
      ;;
  esac
else
  check_file "$HEAP_FILE"
  case "$ML_PLATFORM" in
    *-windows)
      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
      ;;
    *)
      PLATFORM_HEAP_FILE="$HEAP_FILE"
      ;;
  esac
  PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")"
  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success)"
fi


## 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"


## ML text

if [ -n "$MODES" ]; then
  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Unsynchronized.change print_mode (append [$MODES])"
fi

if [ -n "$SECURE" ]; then
  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()"
fi

if [ -n "$PROCESS_SOCKET" ]; then
  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="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
    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()"
  fi
fi


## ML process

check_file "$ML_HOME/poly"
librarypath "$ML_HOME"

export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS

if [ -n "$TERMINATE" ]; then
  "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \
    "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null
  RC="$?"
else
  "$ISABELLE_HOME/lib/scripts/feeder" -p | \
    {
      read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
      RC="$?"
      kill -TERM "$FPID"
      exit "$RC"
    }
  RC="$?"
fi

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

exit "$RC"