bin/isabelle-process
author wenzelm
Sun May 12 13:46:41 2013 +0200 (2013-05-12)
changeset 51938 cf9c8d8d8939
parent 51932 f196352201d6
child 51948 cb5dbc9a06f9
permissions -rwxr-xr-x
Proof General interaction always uses Isar loop;
pass Isabelle/Scala options to Proof General process as well;
     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 "    -f           pass 'Session.finish();' to the ML session"
    36   echo "    -m MODE      add print mode for output"
    37   echo "    -q           non-interactive session"
    38   echo "    -r           open heap file read-only"
    39   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    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=false
    62 PROOFGENERAL=""
    63 SECURE=""
    64 WRAPPER_SOCKET=""
    65 WRAPPER_FIFOS=""
    66 MLTEXT=""
    67 MODES=""
    68 TERMINATE=""
    69 READONLY=""
    70 NOWRITE=""
    71 
    72 while getopts "IPST:W:e:fm:qruw" OPT
    73 do
    74   case "$OPT" in
    75     I)
    76       ISAR=true
    77       ;;
    78     P)
    79       ISAR=true
    80       PROOFGENERAL=true
    81       ;;
    82     S)
    83       SECURE=true
    84       ;;
    85     T)
    86       WRAPPER_SOCKET="$OPTARG"
    87       ;;
    88     W)
    89       WRAPPER_FIFOS="$OPTARG"
    90       ;;
    91     e)
    92       MLTEXT="$MLTEXT $OPTARG"
    93       ;;
    94     f)
    95       MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
    96       ;;
    97     m)
    98       if [ -z "$MODES" ]; then
    99         MODES="\"$OPTARG\""
   100       else
   101         MODES="\"$OPTARG\", $MODES"
   102       fi
   103       ;;
   104     q)
   105       TERMINATE=true
   106       ;;
   107     r)
   108       READONLY=true
   109       ;;
   110     u)
   111       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   112       ;;
   113     w)
   114       NOWRITE=true
   115       ;;
   116     \?)
   117       usage
   118       ;;
   119   esac
   120 done
   121 
   122 shift $(($OPTIND - 1))
   123 
   124 
   125 # args
   126 
   127 INPUT=""
   128 OUTPUT=""
   129 
   130 if [ "$#" -ge 1 ]; then
   131   INPUT="$1"
   132   shift
   133 fi
   134 
   135 if [ "$#" -ge 1 ]; then
   136   OUTPUT="$1"
   137   shift
   138 fi
   139 
   140 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   141 
   142 
   143 ## check ML system
   144 
   145 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   146 
   147 
   148 ## input heap file
   149 
   150 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   151 
   152 case "$INPUT" in
   153   RAW_ML_SYSTEM)
   154     INFILE=""
   155     ;;
   156   */*)
   157     INFILE="$INPUT"
   158     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   159     ;;
   160   *)
   161     INFILE=""
   162     ISA_PATH=""
   163 
   164     splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
   165     for DIR in "${PATHS[@]}"
   166     do
   167       DIR="$DIR/$ML_IDENTIFIER"
   168       ISA_PATH="$ISA_PATH  $DIR\n"
   169       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   170     done
   171 
   172     if [ -z "$INFILE" ]; then
   173       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   174       echo -ne "$ISA_PATH" >&2
   175       exit 2
   176     fi
   177     ;;
   178 esac
   179 
   180 
   181 ## output heap file
   182 
   183 case "$OUTPUT" in
   184   "")
   185     if [ -z "$READONLY" -a -w "$INFILE" ]; then
   186       perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
   187     fi
   188     ;;
   189   */*)
   190     OUTFILE="$OUTPUT"
   191     ;;
   192   *)
   193     mkdir -p "$ISABELLE_OUTPUT"
   194     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   195     ;;
   196 esac
   197 
   198 
   199 ## prepare tmp directory
   200 
   201 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   202 ISABELLE_PID="$$"
   203 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   204 mkdir -p "$ISABELLE_TMP"
   205 
   206 
   207 ## run it!
   208 
   209 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   210 
   211 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
   212 
   213 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   214 
   215 NICE="nice"
   216 
   217 if [ -n "$WRAPPER_SOCKET" ]; then
   218   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
   219 elif [ -n "$WRAPPER_FIFOS" ]; then
   220   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   221   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   222   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   223   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   224   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
   225 elif [ "$ISAR" = true ]; then
   226   if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
   227     ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   228     "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
   229   fi
   230   if [ -n "$PROOFGENERAL" ]; then
   231     MLTEXT="$MLTEXT; ProofGeneral.init ();"
   232   else
   233     MLTEXT="$MLTEXT; Isar.main ();"
   234   fi
   235 else
   236   NICE=""
   237 fi
   238 
   239 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
   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 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
   249 rmdir "$ISABELLE_TMP"
   250 
   251 exit "$RC"