bin/isabelle-process
author haftmann
Mon Feb 23 21:38:36 2009 +0100 (2009-02-23)
changeset 30076 f3043dafef5f
parent 28935 7c6b0850d240
child 31315 3c7b40548a84
permissions -rwxr-xr-x
improved treatment of case certificates
     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 "    -C           tell ML system to copy output image"
    30   echo "    -I           startup Isar interaction mode"
    31   echo "    -P           startup Proof General interaction mode"
    32   echo "    -S           secure mode -- disallow critical operations"
    33   echo "    -X           startup PGIP interaction mode"
    34   echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
    35   echo "    -c           tell ML system to compress output image"
    36   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    37   echo "    -f           pass 'Session.finish();' to the ML session"
    38   echo "    -m MODE      add print mode for output"
    39   echo "    -q           non-interactive session"
    40   echo "    -r           open heap file read-only"
    41   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    42   echo "    -w           reset write permissions on OUTPUT"
    43   echo
    44   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    45   echo "  These are either names to be searched in the Isabelle path, or"
    46   echo "  actual file names (containing at least one /)."
    47   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    48   echo
    49   exit 1
    50 }
    51 
    52 function fail()
    53 {
    54   echo "$1" >&2
    55   exit 2
    56 }
    57 
    58 
    59 ## process command line
    60 
    61 # options
    62 
    63 COPYDB=""
    64 ISAR=false
    65 PROOFGENERAL=""
    66 SECURE=""
    67 WRAPPER_OUTPUT=""
    68 PGIP=""
    69 COMPRESS=""
    70 MLTEXT=""
    71 MODES=""
    72 TERMINATE=""
    73 READONLY=""
    74 NOWRITE=""
    75 
    76 while getopts "CIPSW:Xce:fm:qruw" OPT
    77 do
    78   case "$OPT" in
    79     C)
    80       COPYDB=true
    81       ;;
    82     I)
    83       ISAR=true
    84       ;;
    85     P)
    86       PROOFGENERAL=true
    87       ;;
    88     S)
    89       SECURE=true
    90       ;;
    91     W)
    92       WRAPPER_OUTPUT="$OPTARG"
    93       ;;
    94     X)
    95       PGIP=true
    96       ;;
    97     c)
    98       COMPRESS=true
    99       ;;
   100     e)
   101       MLTEXT="$MLTEXT $OPTARG"
   102       ;;
   103     f)
   104       MLTEXT="$MLTEXT Session.finish();"
   105       ;;
   106     m)
   107       if [ -z "$MODES" ]; then
   108         MODES="\"$OPTARG\""
   109       else
   110         MODES="\"$OPTARG\", $MODES"
   111       fi
   112       ;;
   113     q)
   114       TERMINATE=true
   115       ;;
   116     r)
   117       READONLY=true
   118       ;;
   119     u)
   120       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   121       ;;
   122     w)
   123       NOWRITE=true
   124       ;;
   125     \?)
   126       usage
   127       ;;
   128   esac
   129 done
   130 
   131 shift $(($OPTIND - 1))
   132 
   133 
   134 # args
   135 
   136 INPUT=""
   137 OUTPUT=""
   138 
   139 if [ "$#" -ge 1 ]; then
   140   INPUT="$1"
   141   shift
   142 fi
   143 
   144 if [ "$#" -ge 1 ]; then
   145   OUTPUT="$1"
   146   shift
   147 fi
   148 
   149 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   150 
   151 
   152 ## check ML system
   153 
   154 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   155 
   156 
   157 ## input heap file
   158 
   159 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   160 
   161 case "$INPUT" in
   162   RAW_ML_SYSTEM)
   163     INFILE=""
   164     ;;
   165   */*)
   166     INFILE="$INPUT"
   167     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   168     ;;
   169   *)
   170     INFILE=""
   171     ISA_PATH=""
   172 
   173     ORIG_IFS="$IFS"
   174     IFS=":"
   175     for DIR in $ISABELLE_PATH
   176     do
   177       DIR="$DIR/$ML_IDENTIFIER"
   178       ISA_PATH="$ISA_PATH  $DIR\n"
   179       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   180     done
   181     IFS="$ORIG_IFS"
   182 
   183     if [ -z "$INFILE" ]; then
   184       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   185       echo -ne "$ISA_PATH" >&2
   186       exit 2
   187     fi
   188     ;;
   189 esac
   190 
   191 
   192 ## output heap file
   193 
   194 case "$OUTPUT" in
   195   "")
   196     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   197     ;;
   198   */*)
   199     OUTFILE="$OUTPUT"
   200     ;;
   201   *)
   202     mkdir -p "$ISABELLE_OUTPUT"
   203     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   204     ;;
   205 esac
   206 
   207 
   208 ## prepare tmp directory
   209 
   210 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   211 ISABELLE_PID="$$"
   212 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   213 mkdir -p "$ISABELLE_TMP"
   214 
   215 
   216 ## run it!
   217 
   218 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   219 
   220 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   221 
   222 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   223 
   224 NICE="nice"
   225 if [ -n "$WRAPPER_OUTPUT" ]; then
   226   [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
   227   MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
   228 elif [ -n "$PGIP" ]; then
   229   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   230 elif [ -n "$PROOFGENERAL" ]; then
   231   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   232 elif [ "$ISAR" = true ]; then
   233   MLTEXT="$MLTEXT; Isar.main();"
   234 else
   235   NICE=""
   236 fi
   237 
   238 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
   239   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"