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