bin/isabelle-process
author wenzelm
Sat Dec 15 17:53:32 2007 +0100 (2007-12-15)
changeset 25645 b2ed983a5e80
parent 25523 08b0feb07239
child 27201 e0323036bcf2
permissions -rwxr-xr-x
non-ML session: run with 'nice', to prevent isabelle process from flooding interactive front-ends (ProofGeneral/XEmacs etc.)
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # Isabelle process startup script.
     7 
     8 if [ -L "$0" ]; then
     9   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
    10   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    11 fi
    12 
    13 
    14 ## settings
    15 
    16 PRG="$(basename "$0")"
    17 
    18 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    19 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    20 
    21 
    22 ## diagnostics
    23 
    24 function usage()
    25 {
    26   echo
    27   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    28   echo
    29   echo "  Options are:"
    30   echo "    -C           tell ML system to copy output image"
    31   echo "    -I           startup Isar interaction mode"
    32   echo "    -P           startup Proof General interaction mode"
    33   echo "    -S           secure mode -- disallow critical operations"
    34   echo "    -X           startup PGIP interaction mode"
    35   echo "    -W           startup process wrapper (interaction via external program)"
    36   echo "    -c           tell ML system to compress output image"
    37   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    38   echo "    -f           pass 'Session.finish();' to the ML session"
    39   echo "    -m MODE      add print mode for output"
    40   echo "    -q           non-interactive session"
    41   echo "    -r           open heap file read-only"
    42   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    43   echo "    -w           reset write permissions on OUTPUT"
    44   echo
    45   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    46   echo "  These are either names to be searched in the Isabelle path, or"
    47   echo "  actual file names (containing at least one /)."
    48   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    49   echo
    50   exit 1
    51 }
    52 
    53 function fail()
    54 {
    55   echo "$1" >&2
    56   exit 2
    57 }
    58 
    59 
    60 ## process command line
    61 
    62 # options
    63 
    64 COPYDB=""
    65 ISAR=false
    66 PROOFGENERAL=""
    67 SECURE=""
    68 WRAPPER=""
    69 PGIP=""
    70 COMPRESS=""
    71 MLTEXT=""
    72 MODES=""
    73 TERMINATE=""
    74 READONLY=""
    75 NOWRITE=""
    76 
    77 while getopts "CIPSWXce:fm:qruw" OPT
    78 do
    79   case "$OPT" in
    80     C)
    81       COPYDB=true
    82       ;;
    83     I)
    84       ISAR=true
    85       ;;
    86     P)
    87       PROOFGENERAL=true
    88       ;;
    89     S)
    90       SECURE=true
    91       ;;
    92     W)
    93       WRAPPER=true
    94       ;;
    95     X)
    96       PGIP=true
    97       ;;
    98     c)
    99       COMPRESS=true
   100       ;;
   101     e)
   102       MLTEXT="$MLTEXT $OPTARG"
   103       ;;
   104     f)
   105       MLTEXT="$MLTEXT Session.finish();"
   106       ;;
   107     m)
   108       if [ -z "$MODES" ]; then
   109         MODES="\"$OPTARG\""
   110       else
   111         MODES="\"$OPTARG\", $MODES"
   112       fi
   113       ;;
   114     q)
   115       TERMINATE=true
   116       ;;
   117     r)
   118       READONLY=true
   119       ;;
   120     u)
   121       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   122       ;;
   123     w)
   124       NOWRITE=true
   125       ;;
   126     \?)
   127       usage
   128       ;;
   129   esac
   130 done
   131 
   132 shift $(($OPTIND - 1))
   133 
   134 
   135 # args
   136 
   137 INPUT=""
   138 OUTPUT=""
   139 
   140 if [ "$#" -ge 1 ]; then
   141   INPUT="$1"
   142   shift
   143 fi
   144 
   145 if [ "$#" -ge 1 ]; then
   146   OUTPUT="$1"
   147   shift
   148 fi
   149 
   150 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   151 
   152 
   153 ## check ML system
   154 
   155 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   156 
   157 
   158 ## input heap file
   159 
   160 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   161 
   162 case "$INPUT" in
   163   RAW_ML_SYSTEM)
   164     INFILE=""
   165     ;;
   166   */*)
   167     INFILE="$INPUT$ML_SUFFIX"
   168     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   169     ;;
   170   *)
   171     INFILE=""
   172     ISA_PATH=""
   173 
   174     ORIG_IFS="$IFS"
   175     IFS=":"
   176     for DIR in $ISABELLE_PATH
   177     do
   178       DIR="$DIR/$ML_IDENTIFIER"
   179       ISA_PATH="$ISA_PATH  $DIR\n"
   180       [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX"
   181     done
   182     IFS="$ORIG_IFS"
   183 
   184     if [ -z "$INFILE" ]; then
   185       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   186       echo -ne "$ISA_PATH" >&2
   187       exit 2
   188     fi
   189     ;;
   190 esac
   191 
   192 
   193 ## output heap file
   194 
   195 case "$OUTPUT" in
   196   "")
   197     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   198     ;;
   199   */*)
   200     OUTFILE="$OUTPUT$ML_SUFFIX"
   201     ;;
   202   *)
   203     mkdir -p "$ISABELLE_OUTPUT"
   204     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX"
   205     ;;
   206 esac
   207 
   208 
   209 ## prepare tmp directory
   210 
   211 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   212 ISABELLE_PID="$$"
   213 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   214 mkdir -p "$ISABELLE_TMP"
   215 
   216 
   217 ## run it!
   218 
   219 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   220 
   221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   222 
   223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   224 
   225 NICE="nice"
   226 if [ -n "$WRAPPER" ]; then
   227   MLTEXT="$MLTEXT; IsabelleProcess.init();"
   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"