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