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