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