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