bin/isabelle_process
author blanchet
Tue May 20 16:11:37 2014 +0200 (2014-05-20)
changeset 57017 afdf75c0de58
parent 56628 a2df9de46060
child 57581 74bbe9317aa4
permissions -rwxr-xr-x
tuning
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # Isabelle process startup script.
     6 
     7 if [ -L "$0" ]; then
     8   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
     9   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    10 fi
    11 
    12 
    13 ## settings
    14 
    15 PRG="$(basename "$0")"
    16 
    17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    19 
    20 
    21 ## diagnostics
    22 
    23 function usage()
    24 {
    25   echo
    26   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    27   echo
    28   echo "  Options are:"
    29   echo "    -I           startup Isar interaction mode"
    30   echo "    -P           startup Proof General interaction mode"
    31   echo "    -S           secure mode -- disallow critical operations"
    32   echo "    -T ADDR      startup process wrapper, with socket address"
    33   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
    34   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    35   echo "    -m MODE      add print mode for output"
    36   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    37   echo "    -q           non-interactive session"
    38   echo "    -r           open heap file read-only"
    39   echo "    -w           reset write permissions on OUTPUT"
    40   echo
    41   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    42   echo "  These are either names to be searched in the Isabelle path, or"
    43   echo "  actual file names (containing at least one /)."
    44   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    45   echo
    46   exit 1
    47 }
    48 
    49 function fail()
    50 {
    51   echo "$1" >&2
    52   exit 2
    53 }
    54 
    55 
    56 ## process command line
    57 
    58 # options
    59 
    60 ISAR=""
    61 PROOFGENERAL=""
    62 SECURE=""
    63 WRAPPER_SOCKET=""
    64 WRAPPER_FIFOS=""
    65 MLTEXT=""
    66 MODES=""
    67 declare -a SYSTEM_OPTIONS=()
    68 TERMINATE=""
    69 READONLY=""
    70 NOWRITE=""
    71 
    72 while getopts "IPST:W:e:m:o:qrw" OPT
    73 do
    74   case "$OPT" in
    75     I)
    76       ISAR=true
    77       ;;
    78     P)
    79       PROOFGENERAL=true
    80       ;;
    81     S)
    82       SECURE=true
    83       ;;
    84     T)
    85       WRAPPER_SOCKET="$OPTARG"
    86       ;;
    87     W)
    88       WRAPPER_FIFOS="$OPTARG"
    89       ;;
    90     e)
    91       MLTEXT="$MLTEXT $OPTARG"
    92       ;;
    93     m)
    94       if [ -z "$MODES" ]; then
    95         MODES="\"$OPTARG\""
    96       else
    97         MODES="\"$OPTARG\", $MODES"
    98       fi
    99       ;;
   100     o)
   101       SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
   102       ;;
   103     q)
   104       TERMINATE=true
   105       ;;
   106     r)
   107       READONLY=true
   108       ;;
   109     w)
   110       NOWRITE=true
   111       ;;
   112     \?)
   113       usage
   114       ;;
   115   esac
   116 done
   117 
   118 shift $(($OPTIND - 1))
   119 
   120 
   121 # args
   122 
   123 INPUT=""
   124 OUTPUT=""
   125 
   126 if [ "$#" -ge 1 ]; then
   127   INPUT="$1"
   128   shift
   129 fi
   130 
   131 if [ "$#" -ge 1 ]; then
   132   OUTPUT="$1"
   133   shift
   134 fi
   135 
   136 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   137 
   138 
   139 ## check ML system
   140 
   141 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   142 
   143 
   144 ## input heap file
   145 
   146 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   147 
   148 case "$INPUT" in
   149   RAW_ML_SYSTEM)
   150     INFILE=""
   151     ;;
   152   */*)
   153     INFILE="$INPUT"
   154     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   155     ;;
   156   *)
   157     INFILE=""
   158     ISA_PATH=""
   159 
   160     splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
   161     for DIR in "${PATHS[@]}"
   162     do
   163       DIR="$DIR/$ML_IDENTIFIER"
   164       ISA_PATH="$ISA_PATH  $DIR\n"
   165       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   166     done
   167 
   168     if [ -z "$INFILE" ]; then
   169       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   170       echo -ne "$ISA_PATH" >&2
   171       exit 2
   172     fi
   173     ;;
   174 esac
   175 
   176 
   177 ## output heap file
   178 
   179 case "$OUTPUT" in
   180   "")
   181     if [ -z "$READONLY" -a -w "$INFILE" ]; then
   182       perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
   183     fi
   184     ;;
   185   */*)
   186     OUTFILE="$OUTPUT"
   187     ;;
   188   *)
   189     mkdir -p "$ISABELLE_OUTPUT"
   190     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   191     ;;
   192 esac
   193 
   194 
   195 ## prepare tmp directory
   196 
   197 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   198 ISABELLE_PID="$$"
   199 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   200 mkdir -p "$ISABELLE_TMP"
   201 
   202 
   203 ## run it!
   204 
   205 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   206 
   207 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
   208 
   209 [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
   210 
   211 NICE="nice"
   212 
   213 if [ -n "$WRAPPER_SOCKET" ]; then
   214   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
   215 elif [ -n "$WRAPPER_FIFOS" ]; then
   216   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   217   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   218   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   219   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   220   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
   221 else
   222   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   223   "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
   224     fail "Failed to retrieve Isabelle system options"
   225   if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
   226     MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
   227   fi
   228   if [ -n "$PROOFGENERAL" ]; then
   229     MLTEXT="$MLTEXT; ProofGeneral.init ();"
   230   elif [ -n "$ISAR" ]; then
   231     MLTEXT="$MLTEXT; Isar.main ();"
   232   else
   233     NICE=""
   234   fi
   235 fi
   236 
   237 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
   238 
   239 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   240   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   241 else
   242   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   243 fi
   244 RC="$?"
   245 
   246 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
   247 rmdir "$ISABELLE_TMP"
   248 
   249 exit "$RC"