bin/isabelle-process
author wenzelm
Wed Sep 21 22:18:17 2011 +0200 (2011-09-21)
changeset 45028 d608dd8cd409
parent 38253 3d4e521014f7
child 45056 bbd7eac14df3
permissions -rwxr-xr-x
alternative Socket_Channel;
use BinIO for fifos uniformly;
     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 "    -X           startup PGIP interaction mode"
    35   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    36   echo "    -f           pass 'Session.finish();' to the ML session"
    37   echo "    -m MODE      add print mode for output"
    38   echo "    -q           non-interactive session"
    39   echo "    -r           open heap file read-only"
    40   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    41   echo "    -w           reset write permissions on OUTPUT"
    42   echo
    43   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    44   echo "  These are either names to be searched in the Isabelle path, or"
    45   echo "  actual file names (containing at least one /)."
    46   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    47   echo
    48   exit 1
    49 }
    50 
    51 function fail()
    52 {
    53   echo "$1" >&2
    54   exit 2
    55 }
    56 
    57 
    58 ## process command line
    59 
    60 # options
    61 
    62 ISAR=false
    63 PROOFGENERAL=""
    64 SECURE=""
    65 WRAPPER_SOCKET=""
    66 WRAPPER_FIFOS=""
    67 PGIP=""
    68 MLTEXT=""
    69 MODES=""
    70 TERMINATE=""
    71 READONLY=""
    72 NOWRITE=""
    73 
    74 while getopts "IPST:W:Xe:fm:qruw" OPT
    75 do
    76   case "$OPT" in
    77     I)
    78       ISAR=true
    79       ;;
    80     P)
    81       PROOFGENERAL=true
    82       ;;
    83     S)
    84       SECURE=true
    85       ;;
    86     T)
    87       WRAPPER_SOCKET="$OPTARG"
    88       ;;
    89     W)
    90       WRAPPER_FIFOS="$OPTARG"
    91       ;;
    92     X)
    93       PGIP=true
    94       ;;
    95     e)
    96       MLTEXT="$MLTEXT $OPTARG"
    97       ;;
    98     f)
    99       MLTEXT="$MLTEXT Session.finish();"
   100       ;;
   101     m)
   102       if [ -z "$MODES" ]; then
   103         MODES="\"$OPTARG\""
   104       else
   105         MODES="\"$OPTARG\", $MODES"
   106       fi
   107       ;;
   108     q)
   109       TERMINATE=true
   110       ;;
   111     r)
   112       READONLY=true
   113       ;;
   114     u)
   115       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   116       ;;
   117     w)
   118       NOWRITE=true
   119       ;;
   120     \?)
   121       usage
   122       ;;
   123   esac
   124 done
   125 
   126 shift $(($OPTIND - 1))
   127 
   128 
   129 # args
   130 
   131 INPUT=""
   132 OUTPUT=""
   133 
   134 if [ "$#" -ge 1 ]; then
   135   INPUT="$1"
   136   shift
   137 fi
   138 
   139 if [ "$#" -ge 1 ]; then
   140   OUTPUT="$1"
   141   shift
   142 fi
   143 
   144 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   145 
   146 
   147 ## check ML system
   148 
   149 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   150 
   151 
   152 ## input heap file
   153 
   154 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   155 
   156 case "$INPUT" in
   157   RAW_ML_SYSTEM)
   158     INFILE=""
   159     ;;
   160   */*)
   161     INFILE="$INPUT"
   162     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   163     ;;
   164   *)
   165     INFILE=""
   166     ISA_PATH=""
   167 
   168     splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
   169     for DIR in "${PATHS[@]}"
   170     do
   171       DIR="$DIR/$ML_IDENTIFIER"
   172       ISA_PATH="$ISA_PATH  $DIR\n"
   173       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   174     done
   175 
   176     if [ -z "$INFILE" ]; then
   177       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   178       echo -ne "$ISA_PATH" >&2
   179       exit 2
   180     fi
   181     ;;
   182 esac
   183 
   184 
   185 ## output heap file
   186 
   187 case "$OUTPUT" in
   188   "")
   189     if [ -z "$READONLY" -a -w "$INFILE" ]; then
   190       perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
   191     fi
   192     ;;
   193   */*)
   194     OUTFILE="$OUTPUT"
   195     ;;
   196   *)
   197     mkdir -p "$ISABELLE_OUTPUT"
   198     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   199     ;;
   200 esac
   201 
   202 
   203 ## prepare tmp directory
   204 
   205 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   206 ISABELLE_PID="$$"
   207 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   208 mkdir -p "$ISABELLE_TMP"
   209 
   210 
   211 ## run it!
   212 
   213 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   214 
   215 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   216 
   217 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   218 
   219 NICE="nice"
   220 
   221 if [ -n "$WRAPPER_SOCKET" ]; then
   222   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
   223 elif [ -n "$WRAPPER_FIFOS" ]; then
   224   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   225   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   226   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   227   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   228   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
   229 elif [ -n "$PGIP" ]; then
   230   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   231 elif [ -n "$PROOFGENERAL" ]; then
   232   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   233 elif [ "$ISAR" = true ]; then
   234   MLTEXT="$MLTEXT; Isar.main();"
   235 else
   236   NICE=""
   237 fi
   238 
   239 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
   240 
   241 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   242   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   243 else
   244   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   245 fi
   246 RC="$?"
   247 
   248 rmdir "$ISABELLE_TMP"
   249 
   250 exit "$RC"