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