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