smart selection of isabelle-process versus isabelle-interface;
authorwenzelm
Sat Sep 08 20:00:31 2001 +0200 (2001-09-08)
changeset 11550915c5de6480f
parent 11549 e7265e70fd7c
child 11551 8b5064d1c5c9
smart selection of isabelle-process versus isabelle-interface;
bin/isabelle
bin/isabelle-interface
bin/isabelle-process
lib/Tools/install
     1.1 --- a/bin/isabelle	Tue Sep 04 21:10:57 2001 +0200
     1.2 +++ b/bin/isabelle	Sat Sep 08 20:00:31 2001 +0200
     1.3 @@ -4,220 +4,12 @@
     1.4  # Author: Markus Wenzel, TU Muenchen
     1.5  # License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.6  #
     1.7 -# Basic Isabelle startup script.
     1.8 -
     1.9 -
    1.10 -## settings
    1.11 -
    1.12 -PRG="$(basename "$0")"
    1.13 -
    1.14 -ISABELLE_HOME="$(dirname "$0")/.."
    1.15 -. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    1.16 -  { echo "$PRG probably not called from its original place!"; exit 2; }
    1.17 -
    1.18 -
    1.19 -## diagnostics
    1.20 -
    1.21 -function usage()
    1.22 -{
    1.23 -  echo
    1.24 -  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    1.25 -  echo
    1.26 -  echo "  Options are:"
    1.27 -  echo "    -C           tell ML system to copy output image"
    1.28 -  echo "    -I           startup Isar interaction mode"
    1.29 -  echo "    -P           startup Proof General interaction mode"
    1.30 -  echo "    -c           tell ML system to compress output image"
    1.31 -  echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.32 -  echo "    -f           pass 'Session.finish();' to the ML session"
    1.33 -  echo "    -m MODE      add print mode for output"
    1.34 -  echo "    -q           non-interactive session"
    1.35 -  echo "    -r           open heap file read-only"
    1.36 -  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    1.37 -  echo "    -w           reset write permissions on OUTPUT"
    1.38 -  echo
    1.39 -  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    1.40 -  echo "  These are either names to be searched in the Isabelle path, or"
    1.41 -  echo "  actual file names (containing at least one /)."
    1.42 -  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    1.43 -  echo
    1.44 -  exit 1
    1.45 -}
    1.46 -
    1.47 -function fail()
    1.48 -{
    1.49 -  echo "$1" >&2
    1.50 -  exit 2
    1.51 -}
    1.52 -
    1.53 -
    1.54 -## process command line
    1.55 -
    1.56 -# options
    1.57 +# Smart selection of isabelle-process versus isabelle-interface.
    1.58  
    1.59 -COPYDB=""
    1.60 -ISAR=false
    1.61 -PROOFGENERAL=""
    1.62 -COMPRESS=""
    1.63 -MLTEXT=""
    1.64 -MODES=""
    1.65 -TERMINATE=""
    1.66 -READONLY=""
    1.67 -NOWRITE=""
    1.68 -
    1.69 -while getopts "CIPce:fm:qruw" OPT
    1.70 -do
    1.71 -  case "$OPT" in
    1.72 -    C)
    1.73 -      COPYDB=true
    1.74 -      ;;
    1.75 -    I)
    1.76 -      ISAR=true
    1.77 -      ;;
    1.78 -    P)
    1.79 -      PROOFGENERAL=true
    1.80 -      ;;
    1.81 -    c)
    1.82 -      COMPRESS=true
    1.83 -      ;;
    1.84 -    e)
    1.85 -      MLTEXT="$MLTEXT $OPTARG"
    1.86 -      ;;
    1.87 -    f)
    1.88 -      MLTEXT="$MLTEXT Session.finish();"
    1.89 -      ;;
    1.90 -    m)
    1.91 -      if [ -z "$MODES" ]; then
    1.92 -        MODES="\"$OPTARG\""
    1.93 -      else
    1.94 -        MODES="\"$OPTARG\", $MODES"
    1.95 -      fi
    1.96 -      ;;
    1.97 -    q)
    1.98 -      TERMINATE=true
    1.99 -      ;;
   1.100 -    r)
   1.101 -      READONLY=true
   1.102 -      ;;
   1.103 -    u)
   1.104 -      MLTEXT="$MLTEXT use\"ROOT.ML\";"
   1.105 -      ;;
   1.106 -    w)
   1.107 -      NOWRITE=true
   1.108 -      ;;
   1.109 -    \?)
   1.110 -      usage
   1.111 -      ;;
   1.112 -  esac
   1.113 -done
   1.114 -
   1.115 -shift $(($OPTIND - 1))
   1.116 +THIS=$(cd "$(dirname "$0")"; pwd)
   1.117 +NAME="$(basename "$0")"
   1.118  
   1.119 -
   1.120 -# args
   1.121 -
   1.122 -INPUT=""
   1.123 -OUTPUT=""
   1.124 -
   1.125 -if [ "$#" -ge 1 ]; then
   1.126 -  INPUT="$1"
   1.127 -  shift
   1.128 -fi
   1.129 -
   1.130 -if [ "$#" -ge 1 ]; then
   1.131 -  OUTPUT="$1"
   1.132 -  shift
   1.133 -fi
   1.134 -
   1.135 -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   1.136 -
   1.137 -
   1.138 -## check ML system
   1.139 -
   1.140 -[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   1.141 -
   1.142 -
   1.143 -## input heap file
   1.144 -
   1.145 -[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   1.146 -
   1.147 -case "$INPUT" in
   1.148 -  RAW_ML_SYSTEM)
   1.149 -    INFILE=""
   1.150 -    ;;
   1.151 -  */*)
   1.152 -    INFILE="$INPUT"
   1.153 -    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   1.154 -    ;;
   1.155 -  *)
   1.156 -    INFILE=""
   1.157 -    ISA_PATH=""
   1.158 -
   1.159 -    ORIG_IFS="$IFS"
   1.160 -    IFS=":"
   1.161 -    for DIR in $ISABELLE_PATH
   1.162 -    do
   1.163 -      DIR="$DIR/$ML_IDENTIFIER"
   1.164 -      ISA_PATH="$ISA_PATH  $DIR\n"
   1.165 -      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   1.166 -    done
   1.167 -    IFS="$ORIG_IFS"
   1.168 +PRG=isabelle-interface
   1.169 +[ "$NAME" = isabelle ] && PRG=isabelle-process
   1.170  
   1.171 -    if [ -z "$INFILE" ]; then
   1.172 -      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   1.173 -      echo -ne "$ISA_PATH" >&2
   1.174 -      exit 2
   1.175 -    fi
   1.176 -    ;;
   1.177 -esac
   1.178 -
   1.179 -
   1.180 -## output heap file
   1.181 -
   1.182 -case "$OUTPUT" in
   1.183 -  "")
   1.184 -    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   1.185 -    ;;
   1.186 -  */*)
   1.187 -    OUTFILE="$OUTPUT"
   1.188 -    ;;
   1.189 -  *)
   1.190 -    mkdir -p "$ISABELLE_OUTPUT"
   1.191 -    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   1.192 -    ;;
   1.193 -esac
   1.194 -
   1.195 -
   1.196 -## prepare tmp directory
   1.197 -
   1.198 -[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   1.199 -
   1.200 -ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   1.201 -mkdir -p "$ISABELLE_TMP"
   1.202 -
   1.203 -
   1.204 -## run it!
   1.205 -
   1.206 -ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   1.207 -
   1.208 -[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   1.209 -
   1.210 -if [ -n "$PROOFGENERAL" ]; then
   1.211 -  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   1.212 -elif [ "$ISAR" = true ]; then
   1.213 -  MLTEXT="$MLTEXT; Isar.main();"
   1.214 -fi
   1.215 -
   1.216 -export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   1.217 -
   1.218 -if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   1.219 -  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   1.220 -else
   1.221 -  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   1.222 -fi
   1.223 -RC="$?"
   1.224 -
   1.225 -#Do not even think of 'rm -r'!!
   1.226 -rmdir "$ISABELLE_TMP"
   1.227 -
   1.228 -exit "$RC"
   1.229 +exec "$THIS/$PRG" "$@"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/bin/isabelle-interface	Sat Sep 08 20:00:31 2001 +0200
     2.3 @@ -0,0 +1,44 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Markus Wenzel, TU Muenchen
     2.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.9 +#
    2.10 +# Isabelle interface startup script.
    2.11 +
    2.12 +
    2.13 +## settings
    2.14 +
    2.15 +PRG="$(basename "$0")"
    2.16 +
    2.17 +ISABELLE_HOME="$(dirname "$0")/.."
    2.18 +. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    2.19 +  { echo "$PRG probably not called from its original place!"; exit 2; }
    2.20 +
    2.21 +
    2.22 +## diagnostics
    2.23 +
    2.24 +function fail()
    2.25 +{
    2.26 +  echo "$1" >&2
    2.27 +  exit 2
    2.28 +}
    2.29 +
    2.30 +
    2.31 +## main
    2.32 +
    2.33 +case "$ISABELLE_INTERFACE" in
    2.34 +  none)
    2.35 +    INTERFACE="$ISABELLE"
    2.36 +    ;;
    2.37 +  */*)
    2.38 +    INTERFACE="$ISABELLE_INTERFACE"
    2.39 +    ;;
    2.40 +  *)
    2.41 +    INTERFACE="$ISABELLE_HOME/lib/scripts/isa-$ISABELLE_INTERFACE"
    2.42 +    ;;
    2.43 +esac
    2.44 +
    2.45 +[ ! -x "$INTERFACE" ] && fail "Bad Isabelle interface: \"$ISABELLE_INTERFACE\""
    2.46 +
    2.47 +exec "$INTERFACE" "$@"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/bin/isabelle-process	Sat Sep 08 20:00:31 2001 +0200
     3.3 @@ -0,0 +1,222 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# $Id$
     3.7 +# Author: Markus Wenzel, TU Muenchen
     3.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     3.9 +#
    3.10 +# Isabelle process startup script.
    3.11 +
    3.12 +
    3.13 +## settings
    3.14 +
    3.15 +PRG="$(basename "$0")"
    3.16 +
    3.17 +ISABELLE_HOME="$(dirname "$0")/.."
    3.18 +. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    3.19 +  { echo "$PRG probably not called from its original place!"; exit 2; }
    3.20 +
    3.21 +
    3.22 +## diagnostics
    3.23 +
    3.24 +function usage()
    3.25 +{
    3.26 +  echo
    3.27 +  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    3.28 +  echo
    3.29 +  echo "  Options are:"
    3.30 +  echo "    -C           tell ML system to copy output image"
    3.31 +  echo "    -I           startup Isar interaction mode"
    3.32 +  echo "    -P           startup Proof General interaction mode"
    3.33 +  echo "    -c           tell ML system to compress output image"
    3.34 +  echo "    -e MLTEXT    pass MLTEXT to the ML session"
    3.35 +  echo "    -f           pass 'Session.finish();' to the ML session"
    3.36 +  echo "    -m MODE      add print mode for output"
    3.37 +  echo "    -q           non-interactive session"
    3.38 +  echo "    -r           open heap file read-only"
    3.39 +  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    3.40 +  echo "    -w           reset write permissions on OUTPUT"
    3.41 +  echo
    3.42 +  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    3.43 +  echo "  These are either names to be searched in the Isabelle path, or"
    3.44 +  echo "  actual file names (containing at least one /)."
    3.45 +  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    3.46 +  echo
    3.47 +  exit 1
    3.48 +}
    3.49 +
    3.50 +function fail()
    3.51 +{
    3.52 +  echo "$1" >&2
    3.53 +  exit 2
    3.54 +}
    3.55 +
    3.56 +
    3.57 +## process command line
    3.58 +
    3.59 +# options
    3.60 +
    3.61 +COPYDB=""
    3.62 +ISAR=false
    3.63 +PROOFGENERAL=""
    3.64 +COMPRESS=""
    3.65 +MLTEXT=""
    3.66 +MODES=""
    3.67 +TERMINATE=""
    3.68 +READONLY=""
    3.69 +NOWRITE=""
    3.70 +
    3.71 +while getopts "CIPce:fm:qruw" OPT
    3.72 +do
    3.73 +  case "$OPT" in
    3.74 +    C)
    3.75 +      COPYDB=true
    3.76 +      ;;
    3.77 +    I)
    3.78 +      ISAR=true
    3.79 +      ;;
    3.80 +    P)
    3.81 +      PROOFGENERAL=true
    3.82 +      ;;
    3.83 +    c)
    3.84 +      COMPRESS=true
    3.85 +      ;;
    3.86 +    e)
    3.87 +      MLTEXT="$MLTEXT $OPTARG"
    3.88 +      ;;
    3.89 +    f)
    3.90 +      MLTEXT="$MLTEXT Session.finish();"
    3.91 +      ;;
    3.92 +    m)
    3.93 +      if [ -z "$MODES" ]; then
    3.94 +        MODES="\"$OPTARG\""
    3.95 +      else
    3.96 +        MODES="\"$OPTARG\", $MODES"
    3.97 +      fi
    3.98 +      ;;
    3.99 +    q)
   3.100 +      TERMINATE=true
   3.101 +      ;;
   3.102 +    r)
   3.103 +      READONLY=true
   3.104 +      ;;
   3.105 +    u)
   3.106 +      MLTEXT="$MLTEXT use\"ROOT.ML\";"
   3.107 +      ;;
   3.108 +    w)
   3.109 +      NOWRITE=true
   3.110 +      ;;
   3.111 +    \?)
   3.112 +      usage
   3.113 +      ;;
   3.114 +  esac
   3.115 +done
   3.116 +
   3.117 +shift $(($OPTIND - 1))
   3.118 +
   3.119 +
   3.120 +# args
   3.121 +
   3.122 +INPUT=""
   3.123 +OUTPUT=""
   3.124 +
   3.125 +if [ "$#" -ge 1 ]; then
   3.126 +  INPUT="$1"
   3.127 +  shift
   3.128 +fi
   3.129 +
   3.130 +if [ "$#" -ge 1 ]; then
   3.131 +  OUTPUT="$1"
   3.132 +  shift
   3.133 +fi
   3.134 +
   3.135 +[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   3.136 +
   3.137 +
   3.138 +## check ML system
   3.139 +
   3.140 +[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   3.141 +
   3.142 +
   3.143 +## input heap file
   3.144 +
   3.145 +[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   3.146 +
   3.147 +case "$INPUT" in
   3.148 +  RAW_ML_SYSTEM)
   3.149 +    INFILE=""
   3.150 +    ;;
   3.151 +  */*)
   3.152 +    INFILE="$INPUT"
   3.153 +    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   3.154 +    ;;
   3.155 +  *)
   3.156 +    INFILE=""
   3.157 +    ISA_PATH=""
   3.158 +
   3.159 +    ORIG_IFS="$IFS"
   3.160 +    IFS=":"
   3.161 +    for DIR in $ISABELLE_PATH
   3.162 +    do
   3.163 +      DIR="$DIR/$ML_IDENTIFIER"
   3.164 +      ISA_PATH="$ISA_PATH  $DIR\n"
   3.165 +      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   3.166 +    done
   3.167 +    IFS="$ORIG_IFS"
   3.168 +
   3.169 +    if [ -z "$INFILE" ]; then
   3.170 +      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   3.171 +      echo -ne "$ISA_PATH" >&2
   3.172 +      exit 2
   3.173 +    fi
   3.174 +    ;;
   3.175 +esac
   3.176 +
   3.177 +
   3.178 +## output heap file
   3.179 +
   3.180 +case "$OUTPUT" in
   3.181 +  "")
   3.182 +    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   3.183 +    ;;
   3.184 +  */*)
   3.185 +    OUTFILE="$OUTPUT"
   3.186 +    ;;
   3.187 +  *)
   3.188 +    mkdir -p "$ISABELLE_OUTPUT"
   3.189 +    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   3.190 +    ;;
   3.191 +esac
   3.192 +
   3.193 +
   3.194 +## prepare tmp directory
   3.195 +
   3.196 +[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   3.197 +
   3.198 +ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   3.199 +mkdir -p "$ISABELLE_TMP"
   3.200 +
   3.201 +
   3.202 +## run it!
   3.203 +
   3.204 +ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   3.205 +
   3.206 +[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   3.207 +
   3.208 +if [ -n "$PROOFGENERAL" ]; then
   3.209 +  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   3.210 +elif [ "$ISAR" = true ]; then
   3.211 +  MLTEXT="$MLTEXT; Isar.main();"
   3.212 +fi
   3.213 +
   3.214 +export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   3.215 +
   3.216 +if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   3.217 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   3.218 +else
   3.219 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   3.220 +fi
   3.221 +RC="$?"
   3.222 +
   3.223 +rmdir "$ISABELLE_TMP"
   3.224 +
   3.225 +exit "$RC"
     4.1 --- a/lib/Tools/install	Tue Sep 04 21:10:57 2001 +0200
     4.2 +++ b/lib/Tools/install	Sat Sep 08 20:00:31 2001 +0200
     4.3 @@ -95,7 +95,7 @@
     4.4  if [ -n "$BINDIR" ]; then
     4.5    mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
     4.6  
     4.7 -  for NAME in isatool isabelle Isabelle
     4.8 +  for NAME in isatool isabelle-process isabelle-interface
     4.9    do
    4.10      BIN="$BINDIR/$NAME"
    4.11      DIST="$DISTDIR/bin/$NAME"
    4.12 @@ -105,6 +105,14 @@
    4.13      echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    4.14      chmod +x "$BIN"
    4.15    done
    4.16 +  for NAME in Isabelle isabelle
    4.17 +  do
    4.18 +    BIN="$BINDIR/$NAME"
    4.19 +    DIST="$DISTDIR/bin/$NAME"
    4.20 +    echo "installing $BIN"
    4.21 +    cp "$DIST" "$BIN" || fail "Cannot write file: $BIN"
    4.22 +    chmod +x "$BIN"
    4.23 +  done
    4.24  fi
    4.25  
    4.26  
    4.27 @@ -138,7 +146,7 @@
    4.28    echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
    4.29    echo "[KDE Desktop Entry]" >> "$KDEAPP"
    4.30    echo "Type=Application" >> "$KDEAPP"
    4.31 -  echo "Exec=\"$DISTDIR/bin/Isabelle\" %f" >> "$KDEAPP"
    4.32 +  echo "Exec=\"$DISTDIR/bin/isabelle-interface\" %f" >> "$KDEAPP"
    4.33    echo "Icon=isabelle.xpm" >> "$KDEAPP"
    4.34    echo "TerminalOptions=" >> "$KDEAPP"
    4.35    echo "Path=" >> "$KDEAPP"