bin/isabelle
author wenzelm
Fri Sep 15 16:28:04 2000 +0200 (2000-09-15)
changeset 9972 05afcc505da3
parent 9786 270ca580b880
child 9982 1860276fc8de
permissions -rwxr-xr-x
-P option;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # Basic Isabelle 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 "    -I           startup Isar interaction mode"
    28   echo "    -P           startup ProofGeneral interaction mode"
    29   echo "    -c           tell ML system to compress output image"
    30   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    31   echo "    -m MODE      add print mode for output"
    32   echo "    -q           non-interactive session"
    33   echo "    -r           open heap file read-only"
    34   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    35   echo "    -w           reset write permissions on OUTPUT"
    36   echo
    37   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    38   echo "  These are either names to be searched in the Isabelle path, or"
    39   echo "  actual file names (containing at least one /)."
    40   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    41   echo
    42   exit 1
    43 }
    44 
    45 function fail()
    46 {
    47   echo "$1" >&2
    48   exit 2
    49 }
    50 
    51 
    52 ## process command line
    53 
    54 # options
    55 
    56 ISAR=false
    57 PROOFGENERAL=""
    58 COMPRESS=""
    59 MLTEXT=""
    60 MODES=""
    61 TERMINATE=""
    62 READONLY=""
    63 NOWRITE=""
    64 
    65 while getopts "IPce:m:qruw" OPT
    66 do
    67   case "$OPT" in
    68     I)
    69       ISAR=true
    70       ;;
    71     P)
    72       PROOFGENERAL=true
    73       ;;
    74     c)
    75       COMPRESS=true
    76       ;;
    77     e)
    78       MLTEXT="$MLTEXT $OPTARG"
    79       ;;
    80     m)
    81       if [ -z "$MODES" ]; then
    82         MODES="\"$OPTARG\""
    83       else
    84         MODES="$MODES, \"$OPTARG\""
    85       fi
    86       ;;
    87     q)
    88       TERMINATE=true
    89       ;;
    90     r)
    91       READONLY=true
    92       ;;
    93     u)
    94       MLTEXT="$MLTEXT use\"ROOT.ML\";"
    95       ;;
    96     w)
    97       NOWRITE=true
    98       ;;
    99     \?)
   100       usage
   101       ;;
   102   esac
   103 done
   104 
   105 shift $(($OPTIND - 1))
   106 
   107 
   108 # args
   109 
   110 INPUT=""
   111 OUTPUT=""
   112 
   113 if [ "$#" -ge 1 ]; then
   114   INPUT="$1"
   115   shift
   116 fi
   117 
   118 if [ "$#" -ge 1 ]; then
   119   OUTPUT="$1"
   120   shift
   121 fi
   122 
   123 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   124 
   125 
   126 ## check ML system
   127 
   128 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   129 
   130 
   131 ## input heap file
   132 
   133 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   134 
   135 case "$INPUT" in
   136   RAW_ML_SYSTEM)
   137     INFILE=""
   138     ;;
   139   */*)
   140     INFILE="$INPUT"
   141     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   142     ;;
   143   *)
   144     INFILE=""
   145     ISA_PATH=""
   146 
   147     ORIG_IFS="$IFS"
   148     IFS=":"
   149     for DIR in $ISABELLE_PATH
   150     do
   151       DIR="$DIR/$ML_IDENTIFIER"
   152       ISA_PATH="$ISA_PATH  $DIR\n"
   153       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   154     done
   155     IFS="$ORIG_IFS"
   156 
   157     if [ -z "$INFILE" ]; then
   158       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   159       echo -ne "$ISA_PATH" >&2
   160       exit 2
   161     fi
   162     ;;
   163 esac
   164 
   165 
   166 ## output heap file
   167 
   168 case "$OUTPUT" in
   169   "")
   170     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   171     ;;
   172   */*)
   173     OUTFILE="$OUTPUT"
   174     ;;
   175   *)
   176     mkdir -p "$ISABELLE_OUTPUT"
   177     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   178     ;;
   179 esac
   180 
   181 
   182 ## prepare tmp directory
   183 
   184 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   185 
   186 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   187 mkdir -p "$ISABELLE_TMP"
   188 
   189 
   190 ## run it!
   191 
   192 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   193 
   194 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   195 
   196 if [ -n "$PROOFGENERAL" ]; then
   197   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   198 elif [ "$ISAR" = true ]; then
   199   MLTEXT="$MLTEXT; Isar.main();"
   200 fi
   201 
   202 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   203 
   204 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   205   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   206 else
   207   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   208 fi
   209 RC="$?"
   210 
   211 #Do not even think of 'rm -r'!!
   212 rmdir "$ISABELLE_TMP"
   213 
   214 exit "$RC"