lib/scripts/run-polyml-5.3.0

isabelle_process executable no longer supports writable heap images;

#!/usr/bin/env bash
#
# Author: Makarius
#
# Startup script for Poly/ML 5.3.0.

export -n HEAP_FILE ML_TEXT TERMINATE


## diagnostics

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

function check_file()
{
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
}


## prepare databases

if [ -z "$HEAP_FILE" ]; then
  INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
else
  check_file "$HEAP_FILE"
  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
fi


## poly process

ML_TEXT="$INIT $ML_TEXT"

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

if [ -z "$TERMINATE" ]; then
  FEEDER_OPTS=""
else
  FEEDER_OPTS="-q"
fi

"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
  { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
RC="$?"

exit "$RC"

#:wrap=soft:maxLineLen=100: