bin/isabelle
author wenzelm
Wed Mar 08 17:39:08 2000 +0100 (2000-03-08)
changeset 8359 124ad46105dd
parent 7887 eedfff88ee40
child 9786 270ca580b880
permissions -rwxr-xr-x
option -c: tell ML system to compress output image;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # Basic Isabelle startup script.
     6 
     7 
     8 ## settings
     9 
    10 PRG=$(basename $0)
    11 
    12 ISABELLE_HOME=$(dirname $0)/..
    13 . $ISABELLE_HOME/lib/scripts/getsettings || \
    14   { echo "$PRG probably not called from its original place!"; exit 2; }
    15 
    16 
    17 ## diagnostics
    18 
    19 function usage()
    20 {
    21   echo
    22   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    23   echo
    24   echo "  Options are:"
    25   echo "    -I           startup Isar interaction mode"
    26   echo "    -c           tell ML system to compress output image"
    27   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    28   echo "    -m MODE      add print mode for output"
    29   echo "    -q           non-interactive session"
    30   echo "    -r           open heap file read-only"
    31   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    32   echo "    -w           reset write permissions on OUTPUT"
    33   echo
    34   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    35   echo "  These are either names to be searched in the Isabelle path, or"
    36   echo "  actual file names (containing at least one /)."
    37   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    38   echo
    39   exit 1
    40 }
    41 
    42 function fail()
    43 {
    44   echo "$1" >&2
    45   exit 2
    46 }
    47 
    48 
    49 ## process command line
    50 
    51 # options
    52 
    53 COMPRESS=""
    54 MLTEXT=""
    55 MODES=""
    56 TERMINATE=""
    57 READONLY=""
    58 NOWRITE=""
    59 
    60 while getopts "Ice:m:qruw" OPT
    61 do
    62   case "$OPT" in
    63     I)
    64       MLTEXT="$MLTEXT Isar.main();"
    65       ;;
    66     c)
    67       COMPRESS=true
    68       ;;
    69     e)
    70       MLTEXT="$MLTEXT $OPTARG"
    71       ;;
    72     m)
    73       if [ -z "$MODES" ]; then
    74         MODES="\"$OPTARG\""
    75       else
    76         MODES="$MODES, \"$OPTARG\""
    77       fi
    78       ;;
    79     q)
    80       TERMINATE=true
    81       ;;
    82     r)
    83       READONLY=true
    84       ;;
    85     u)
    86       MLTEXT="$MLTEXT use\"ROOT.ML\";"
    87       ;;
    88     w)
    89       NOWRITE=true
    90       ;;
    91     \?)
    92       usage
    93       ;;
    94   esac
    95 done
    96 
    97 shift $(($OPTIND - 1))
    98 
    99 
   100 # args
   101 
   102 INPUT=""
   103 OUTPUT=""
   104 
   105 if [ $# -ge 1 ]; then
   106   INPUT="$1"
   107   shift
   108 fi
   109 
   110 if [ $# -ge 1 ]; then
   111   OUTPUT="$1"
   112   shift
   113 fi
   114 
   115 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
   116 
   117 
   118 ## check ML system
   119 
   120 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   121 
   122 
   123 ## input heap file
   124 
   125 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   126 
   127 case "$INPUT" in
   128   RAW_ML_SYSTEM)
   129     INFILE=""
   130     ;;
   131   */*)
   132     INFILE="$INPUT"
   133     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   134     ;;
   135   *)
   136     ISA_PATH=""
   137     INFILE=""
   138     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   139     do
   140       ISA_PATH="$ISA_PATH $DIR"
   141       [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
   142     done
   143     if [ -z "$INFILE" ]; then
   144       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   145       for DIR in $ISA_PATH
   146       do
   147         echo "  $DIR" >&2
   148       done
   149       exit 2
   150     fi
   151     ;;
   152 esac
   153 
   154 
   155 ## output heap file
   156 
   157 case "$OUTPUT" in
   158   "")
   159     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   160     ;;
   161   */*)
   162     OUTFILE="$OUTPUT"
   163     ;;
   164   *)
   165     mkdir -p "$ISABELLE_OUTPUT"
   166     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   167     ;;
   168 esac
   169 
   170 
   171 ## prepare tmp directory
   172 
   173 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   174 
   175 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   176 mkdir -p "$ISABELLE_TMP"
   177 
   178 
   179 ## run it!
   180 
   181 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   182 
   183 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   184 
   185 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   186 
   187 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
   188   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   189 else
   190   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   191 fi
   192 RC=$?
   193 
   194 #Do not even think of 'rm -r'!!
   195 rmdir $ISABELLE_TMP
   196 
   197 exit $RC