bin/isabelle-process
author aspinall
Fri May 07 13:34:13 2004 +0200 (2004-05-07)
changeset 14712 81362115cedd
parent 11550 915c5de6480f
child 14981 e73f8140af78
permissions -rwxr-xr-x
Add -X option to trigger PGIP interaction mode.
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # Isabelle process startup script.
     8 
     9 
    10 ## settings
    11 
    12 PRG="$(basename "$0")"
    13 
    14 ISABELLE_HOME="$(dirname "$0")/.."
    15 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    16   { echo "$PRG probably not called from its original place!"; exit 2; }
    17 
    18 
    19 ## diagnostics
    20 
    21 function usage()
    22 {
    23   echo
    24   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    25   echo
    26   echo "  Options are:"
    27   echo "    -C           tell ML system to copy output image"
    28   echo "    -I           startup Isar interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
    30   echo "    -X           startup PGIP interaction mode"
    31   echo "    -c           tell ML system to compress output image"
    32   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    33   echo "    -f           pass 'Session.finish();' to the ML session"
    34   echo "    -m MODE      add print mode for output"
    35   echo "    -q           non-interactive session"
    36   echo "    -r           open heap file read-only"
    37   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    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 COPYDB=""
    60 ISAR=false
    61 PROOFGENERAL=""
    62 COMPRESS=""
    63 MLTEXT=""
    64 MODES=""
    65 TERMINATE=""
    66 READONLY=""
    67 NOWRITE=""
    68 
    69 while getopts "XCIPce:fm:qruw" OPT
    70 do
    71   case "$OPT" in
    72     C)
    73       COPYDB=true
    74       ;;
    75     I)
    76       ISAR=true
    77       ;;
    78     P)
    79       PROOFGENERAL=true
    80       ;;
    81     X)
    82       PGIP=true
    83       ;;
    84     c)
    85       COMPRESS=true
    86       ;;
    87     e)
    88       MLTEXT="$MLTEXT $OPTARG"
    89       ;;
    90     f)
    91       MLTEXT="$MLTEXT Session.finish();"
    92       ;;
    93     m)
    94       if [ -z "$MODES" ]; then
    95         MODES="\"$OPTARG\""
    96       else
    97         MODES="\"$OPTARG\", $MODES"
    98       fi
    99       ;;
   100     q)
   101       TERMINATE=true
   102       ;;
   103     r)
   104       READONLY=true
   105       ;;
   106     u)
   107       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   108       ;;
   109     w)
   110       NOWRITE=true
   111       ;;
   112     \?)
   113       usage
   114       ;;
   115   esac
   116 done
   117 
   118 shift $(($OPTIND - 1))
   119 
   120 
   121 # args
   122 
   123 INPUT=""
   124 OUTPUT=""
   125 
   126 if [ "$#" -ge 1 ]; then
   127   INPUT="$1"
   128   shift
   129 fi
   130 
   131 if [ "$#" -ge 1 ]; then
   132   OUTPUT="$1"
   133   shift
   134 fi
   135 
   136 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   137 
   138 
   139 ## check ML system
   140 
   141 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   142 
   143 
   144 ## input heap file
   145 
   146 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   147 
   148 case "$INPUT" in
   149   RAW_ML_SYSTEM)
   150     INFILE=""
   151     ;;
   152   */*)
   153     INFILE="$INPUT"
   154     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   155     ;;
   156   *)
   157     INFILE=""
   158     ISA_PATH=""
   159 
   160     ORIG_IFS="$IFS"
   161     IFS=":"
   162     for DIR in $ISABELLE_PATH
   163     do
   164       DIR="$DIR/$ML_IDENTIFIER"
   165       ISA_PATH="$ISA_PATH  $DIR\n"
   166       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   167     done
   168     IFS="$ORIG_IFS"
   169 
   170     if [ -z "$INFILE" ]; then
   171       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   172       echo -ne "$ISA_PATH" >&2
   173       exit 2
   174     fi
   175     ;;
   176 esac
   177 
   178 
   179 ## output heap file
   180 
   181 case "$OUTPUT" in
   182   "")
   183     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   184     ;;
   185   */*)
   186     OUTFILE="$OUTPUT"
   187     ;;
   188   *)
   189     mkdir -p "$ISABELLE_OUTPUT"
   190     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   191     ;;
   192 esac
   193 
   194 
   195 ## prepare tmp directory
   196 
   197 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   198 
   199 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   200 mkdir -p "$ISABELLE_TMP"
   201 
   202 
   203 ## run it!
   204 
   205 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   206 
   207 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   208 
   209 if [ -n "$PGIP" ]; then
   210   MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
   211 elif [ -n "$PROOFGENERAL" ]; then
   212   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   213 elif [ "$ISAR" = true ]; then
   214   MLTEXT="$MLTEXT; Isar.main();"
   215 fi
   216 
   217 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   218 
   219 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   220   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   221 else
   222   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   223 fi
   224 RC="$?"
   225 
   226 rmdir "$ISABELLE_TMP"
   227 
   228 exit "$RC"