bin/isabelle-process

also support higher-order rules for Z3 proof reconstruction

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# 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] [INPUT] [OUTPUT]"
  echo
  echo "  Options are:"
  echo "    -I           startup Isar interaction mode"
  echo "    -P           startup Proof General interaction mode"
  echo "    -S           secure mode -- disallow critical operations"
  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
  echo "    -X           startup PGIP interaction mode"
  echo "    -e MLTEXT    pass MLTEXT to the ML session"
  echo "    -f           pass 'Session.finish();' to the ML session"
  echo "    -m MODE      add print mode for output"
  echo "    -q           non-interactive session"
  echo "    -r           open heap file read-only"
  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
  echo "    -w           reset write permissions on OUTPUT"
  echo
  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
  echo "  These are either names to be searched in the Isabelle path, or"
  echo "  actual file names (containing at least one /)."
  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
  echo
  exit 1
}

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


## process command line

# options

ISAR=false
PROOFGENERAL=""
SECURE=""
WRAPPER_FIFOS=""
PGIP=""
MLTEXT=""
MODES=""
TERMINATE=""
READONLY=""
NOWRITE=""

while getopts "IPSW:Xe:fm:qruw" OPT
do
  case "$OPT" in
    I)
      ISAR=true
      ;;
    P)
      PROOFGENERAL=true
      ;;
    S)
      SECURE=true
      ;;
    W)
      WRAPPER_FIFOS="$OPTARG"
      ;;
    X)
      PGIP=true
      ;;
    e)
      MLTEXT="$MLTEXT $OPTARG"
      ;;
    f)
      MLTEXT="$MLTEXT Session.finish();"
      ;;
    m)
      if [ -z "$MODES" ]; then
        MODES="\"$OPTARG\""
      else
        MODES="\"$OPTARG\", $MODES"
      fi
      ;;
    q)
      TERMINATE=true
      ;;
    r)
      READONLY=true
      ;;
    u)
      MLTEXT="$MLTEXT use\"ROOT.ML\";"
      ;;
    w)
      NOWRITE=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

INPUT=""
OUTPUT=""

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

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

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


## check ML system

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


## input heap file

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

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

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

    if [ -z "$INFILE" ]; then
      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
      echo -ne "$ISA_PATH" >&2
      exit 2
    fi
    ;;
esac


## output heap file

case "$OUTPUT" in
  "")
    if [ -z "$READONLY" -a -w "$INFILE" ]; then
      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
    fi
    ;;
  */*)
    OUTFILE="$OUTPUT"
    ;;
  *)
    mkdir -p "$ISABELLE_OUTPUT"
    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
    ;;
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"


## run it!

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

[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"

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

NICE="nice"

if [ -n "$WRAPPER_FIFOS" ]; then
  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
  MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
elif [ -n "$PGIP" ]; then
  MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
elif [ -n "$PROOFGENERAL" ]; then
  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
elif [ "$ISAR" = true ]; then
  MLTEXT="$MLTEXT; Isar.main();"
else
  NICE=""
fi

export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP

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

rmdir "$ISABELLE_TMP"

exit "$RC"