bin/isabelle
changeset 2343 2588b63b42ca
parent 2308 641be5ad47af
child 2395 c24a79fe3651
equal deleted inserted replaced
2342:859d72636ce7 2343:2588b63b42ca
     1 #!/bin/bash
     1 #!/bin/bash -norc
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # Basic Isabelle startup script.
     5 # Basic Isabelle startup script.
     6 
     6 
     7 
     7 
     8 ## settings
     8 ## settings
     9 
     9 
    10 ISABELLE_HOME=$(dirname $(dirname $0))
    10 ISABELLE_HOME=$(dirname $(dirname $0))
    11 . $ISABELLE_HOME/lib/scripts/getsettings
    11 . $ISABELLE_HOME/lib/scripts/getsettings
    12 
    12 . $ISABELLE_HOME/lib/scripts/getplatform
    13 #get bash-style platform info
       
    14 unset HOSTTYPE
       
    15 unset OSTYPE
       
    16 PLATFORM=$(bash -noprofile -c 'echo $HOSTTYPE-$OSTYPE')
       
    17 
    13 
    18 
    14 
    19 ## diagnostics
    15 ## diagnostics
    20 
    16 
    21 PRG=$(basename $0)
    17 PRG=$(basename $0)
    25   echo
    21   echo
    26   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    22   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    27   echo
    23   echo
    28   echo "  Options are:"
    24   echo "  Options are:"
    29   echo "    -c           force copying of heap file"
    25   echo "    -c           force copying of heap file"
    30   echo "    -e MLTEXT    pass MLTEXT to ML session"
    26   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    31 #FIXME  echo "    -o OPTIONS   pass options to ML system"
       
    32   echo "    -q           non-interactive session"
    27   echo "    -q           non-interactive session"
    33   echo "    -r           open heap file read-only"
    28   echo "    -r           open heap file read-only"
    34   echo "    -u           pass 'use\"ROOT.ML\" handle _ => exit 1; commit();'"
    29   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    35   echo "                 to the ML session"
       
    36   echo
    30   echo
    37   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    31   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    38   echo "  These are either names to be searched in the Isabelle path, or actual"
    32   echo "  These are either names to be searched in the Isabelle path, or actual"
    39   echo "  file names (containing at least one /)."
    33   echo "  file names (then containing at least one /)."
    40   echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
    34   echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
    41   echo
    35   echo
    42   exit 1
    36   exit 1
    43 }
    37 }
    44 
    38 
    45 function fail()
    39 function fail()
    46 {
    40 {
    47   echo "$1"
    41   echo "$1" >&2
    48   exit 2
    42   exit 2
    49 }
    43 }
    50 
    44 
    51 
    45 
    52 ## process command line
    46 ## process command line
    54 # options
    48 # options
    55 
    49 
    56 COPYDB=""
    50 COPYDB=""
    57 MLTEXT=""
    51 MLTEXT=""
    58 COPYDB=""
    52 COPYDB=""
    59 OPTIONS=""
       
    60 TERMINATE=""
    53 TERMINATE=""
    61 READONLY=""
    54 READONLY=""
    62 
    55 
    63 while getopts "ce:qru" OPT
    56 while getopts "ce:qru" OPT
    64 do
    57 do
    67       COPYDB=true
    60       COPYDB=true
    68       ;;
    61       ;;
    69     e)
    62     e)
    70       MLTEXT="$MLTEXT $OPTARG"
    63       MLTEXT="$MLTEXT $OPTARG"
    71       ;;
    64       ;;
    72     o)
       
    73       OPTIONS="$OPTIONS $OPTARG"
       
    74       ;;
       
    75     q)
    65     q)
    76       TERMINATE=true
    66       TERMINATE=true
    77       ;;
    67       ;;
    78     r)
    68     r)
    79       READONLY=true
    69       READONLY=true
    80       ;;
    70       ;;
    81     u)
    71     u)
    82       MLTEXT="$MLTEXT use\"ROOT.ML\" handle _ => exit 1; commit();"
    72       MLTEXT="$MLTEXT exit_use_dir\".\";"
    83       ;;
    73       ;;
    84     \?)
    74     \?)
    85       usage
    75       usage
    86       ;;
    76       ;;
    87   esac
    77   esac
   103 if [ $# -ge 1 ]; then
    93 if [ $# -ge 1 ]; then
   104   OUTPUT="$1"
    94   OUTPUT="$1"
   105   shift
    95   shift
   106 fi
    96 fi
   107 
    97 
   108 [ $# -ne 0 ] && fail "Bad args: $*"
    98 [ $# -ne 0 ] && { echo "Bad args: $*"; usage }
   109 
    99 
   110 
   100 
   111 ## check ML system
   101 ## check ML system
   112 
   102 
   113 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   103 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   121   SYSTEM)
   111   SYSTEM)
   122     INFILE=""
   112     INFILE=""
   123     ;;
   113     ;;
   124   */*)
   114   */*)
   125     INFILE="$INPUT"
   115     INFILE="$INPUT"
   126     [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
   116     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   127     ;;
   117     ;;
   128   *)
   118   *)
   129     ISA_PATH=""
   119     ISA_PATH=""
   130     INFILE=""
   120     INFILE=""
   131     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   121     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   132     do
   122     do
   133       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
   123       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
   134       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   124       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   135     done
   125     done
   136     if [ -z "$INFILE" ]; then
   126     if [ -z "$INFILE" ]; then
   137       echo "Unknown logic \"$INPUT\" -- no heap file found in:"
   127       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   138       for DIR in $ISA_PATH
   128       for DIR in $ISA_PATH
   139       do
   129       do
   140         echo "  $DIR"
   130         echo "  $DIR" >&2
   141       done
   131       done
   142       exit 2
   132       exit 2
   143     fi
   133     fi
   144     ;;
   134     ;;
   145 esac
   135 esac
   164 
   154 
   165 ## run it!
   155 ## run it!
   166 
   156 
   167 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   157 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   168 
   158 
   169 export INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE
   159 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   170 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   160 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   171 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   161 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE