bin/isabelle-process
author wenzelm
Sun Nov 29 17:23:39 2009 +0100 (2009-11-29)
changeset 33920 d4d430dfabc6
parent 32390 468eff174a77
child 34109 f49d45afa634
permissions -rwxr-xr-x
double check file permissions of write-back image -- more robust for root or administrator on Cygwin;
     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 "    -X           startup PGIP interaction mode"
    33   echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
    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_OUTPUT=""
    65 PGIP=""
    66 MLTEXT=""
    67 MODES=""
    68 TERMINATE=""
    69 READONLY=""
    70 NOWRITE=""
    71 
    72 while getopts "IPSW:Xe:fm:qruw" OPT
    73 do
    74   case "$OPT" in
    75     I)
    76       ISAR=true
    77       ;;
    78     P)
    79       PROOFGENERAL=true
    80       ;;
    81     S)
    82       SECURE=true
    83       ;;
    84     W)
    85       WRAPPER_OUTPUT="$OPTARG"
    86       ;;
    87     X)
    88       PGIP=true
    89       ;;
    90     e)
    91       MLTEXT="$MLTEXT $OPTARG"
    92       ;;
    93     f)
    94       MLTEXT="$MLTEXT Session.finish();"
    95       ;;
    96     m)
    97       if [ -z "$MODES" ]; then
    98         MODES="\"$OPTARG\""
    99       else
   100         MODES="\"$OPTARG\", $MODES"
   101       fi
   102       ;;
   103     q)
   104       TERMINATE=true
   105       ;;
   106     r)
   107       READONLY=true
   108       ;;
   109     u)
   110       MLTEXT="$MLTEXT use\"ROOT.ML\";"
   111       ;;
   112     w)
   113       NOWRITE=true
   114       ;;
   115     \?)
   116       usage
   117       ;;
   118   esac
   119 done
   120 
   121 shift $(($OPTIND - 1))
   122 
   123 
   124 # args
   125 
   126 INPUT=""
   127 OUTPUT=""
   128 
   129 if [ "$#" -ge 1 ]; then
   130   INPUT="$1"
   131   shift
   132 fi
   133 
   134 if [ "$#" -ge 1 ]; then
   135   OUTPUT="$1"
   136   shift
   137 fi
   138 
   139 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   140 
   141 
   142 ## check ML system
   143 
   144 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   145 
   146 
   147 ## input heap file
   148 
   149 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   150 
   151 case "$INPUT" in
   152   RAW_ML_SYSTEM)
   153     INFILE=""
   154     ;;
   155   */*)
   156     INFILE="$INPUT"
   157     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   158     ;;
   159   *)
   160     INFILE=""
   161     ISA_PATH=""
   162 
   163     splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
   164     for DIR in "${PATHS[@]}"
   165     do
   166       DIR="$DIR/$ML_IDENTIFIER"
   167       ISA_PATH="$ISA_PATH  $DIR\n"
   168       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   169     done
   170 
   171     if [ -z "$INFILE" ]; then
   172       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   173       echo -ne "$ISA_PATH" >&2
   174       exit 2
   175     fi
   176     ;;
   177 esac
   178 
   179 
   180 ## output heap file
   181 
   182 case "$OUTPUT" in
   183   "")
   184     if [ -z "$READONLY" -a -w "$INFILE" ]; then
   185       perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
   186     fi
   187     ;;
   188   */*)
   189     OUTFILE="$OUTPUT"
   190     ;;
   191   *)
   192     mkdir -p "$ISABELLE_OUTPUT"
   193     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   194     ;;
   195 esac
   196 
   197 
   198 ## prepare tmp directory
   199 
   200 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   201 ISABELLE_PID="$$"
   202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   203 mkdir -p "$ISABELLE_TMP"
   204 
   205 
   206 ## run it!
   207 
   208 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   209 
   210 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   211 
   212 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   213 
   214 NICE="nice"
   215 if [ -n "$WRAPPER_OUTPUT" ]; then
   216   [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
   217   MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
   218 elif [ -n "$PGIP" ]; then
   219   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   220 elif [ -n "$PROOFGENERAL" ]; then
   221   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   222 elif [ "$ISAR" = true ]; then
   223   MLTEXT="$MLTEXT; Isar.main();"
   224 else
   225   NICE=""
   226 fi
   227 
   228 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
   229 
   230 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   231   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   232 else
   233   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   234 fi
   235 RC="$?"
   236 
   237 rmdir "$ISABELLE_TMP"
   238 
   239 exit "$RC"