isabelle.Build uses ML_Process directly;
authorwenzelm
Wed Mar 09 19:30:09 2016 +0100 (2016-03-09)
changeset 6257327f90319a499
parent 62572 acd17a6ce17d
child 62574 ec382bc689e5
isabelle.Build uses ML_Process directly;
isabelle_process is for batch mode only;
removed unused feeder (already part of "isabelle console");
bin/isabelle_process
lib/scripts/feeder
lib/scripts/feeder.pl
src/Doc/System/Basics.thy
src/HOL/Mirabelle/ex/Ex.thy
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/HOL/Mutabelle/lib/Tools/mutabelle
src/HOL/TPTP/lib/Tools/tptp_graph
src/HOL/TPTP/lib/Tools/tptp_isabelle
src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
src/HOL/TPTP/lib/Tools/tptp_nitpick
src/HOL/TPTP/lib/Tools/tptp_refute
src/HOL/TPTP/lib/Tools/tptp_sledgehammer
src/HOL/TPTP/lib/Tools/tptp_translate
src/Pure/Concurrent/bash.scala
src/Pure/ROOT.ML
src/Pure/System/isabelle_system.scala
src/Pure/System/ml_process.scala
src/Pure/Tools/build.scala
src/Tools/Code/code_ml.ML
     1.1 --- a/bin/isabelle_process	Wed Mar 09 16:53:14 2016 +0100
     1.2 +++ b/bin/isabelle_process	Wed Mar 09 19:30:09 2016 +0100
     1.3 @@ -9,248 +9,10 @@
     1.4    exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
     1.5  fi
     1.6  
     1.7 -
     1.8 -## settings
     1.9 -
    1.10 -PRG="$(basename "$0")"
    1.11 -
    1.12  ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    1.13  source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    1.14  
    1.15  
    1.16 -## diagnostics
    1.17 -
    1.18 -function usage()
    1.19 -{
    1.20 -  echo
    1.21 -  echo "Usage: $PRG [OPTIONS] [HEAP]"
    1.22 -  echo
    1.23 -  echo "  Options are:"
    1.24 -  echo "    -O           system options from given YXML file"
    1.25 -  echo "    -P SOCKET    startup process wrapper via TCP socket"
    1.26 -  echo "    -S           secure mode -- disallow critical operations"
    1.27 -  echo "    -e ML_EXPR   evaluate ML expression on startup"
    1.28 -  echo "    -f ML_FILE   evaluate ML file on startup"
    1.29 -  echo "    -m MODE      add print mode for output"
    1.30 -  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    1.31 -  echo "    -q           non-interactive session"
    1.32 -  echo
    1.33 -  echo "  If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;"
    1.34 -  echo "  if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,"
    1.35 -  echo "  the initial ML heap is used."
    1.36 -  echo
    1.37 -  exit 1
    1.38 -}
    1.39 -
    1.40 -function fail()
    1.41 -{
    1.42 -  echo "$1" >&2
    1.43 -  exit 2
    1.44 -}
    1.45 -
    1.46 -function check_file()
    1.47 -{
    1.48 -  [ ! -f "$1" ] && fail "Bad file: \"$1\""
    1.49 -}
    1.50 -
    1.51 -
    1.52 -## process command line
    1.53 -
    1.54 -# options
    1.55 -
    1.56 -OPTIONS_FILE=""
    1.57 -PROCESS_SOCKET=""
    1.58 -SECURE=""
    1.59 -declare -a LAST_ML_OPTIONS=()
    1.60 -MODES=""
    1.61 -declare -a SYSTEM_OPTIONS=()
    1.62 -TERMINATE=""
    1.63 -
    1.64 -while getopts "O:P:Se:f:m:o:q" OPT
    1.65 -do
    1.66 -  case "$OPT" in
    1.67 -    O)
    1.68 -      OPTIONS_FILE="$OPTARG"
    1.69 -      ;;
    1.70 -    P)
    1.71 -      PROCESS_SOCKET="$OPTARG"
    1.72 -      ;;
    1.73 -    S)
    1.74 -      SECURE=true
    1.75 -      ;;
    1.76 -    e)
    1.77 -      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
    1.78 -      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
    1.79 -      ;;
    1.80 -    f)
    1.81 -      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use"
    1.82 -      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
    1.83 -      ;;
    1.84 -    m)
    1.85 -      if [ -z "$MODES" ]; then
    1.86 -        MODES="\"$OPTARG\""
    1.87 -      else
    1.88 -        MODES="\"$OPTARG\", $MODES"
    1.89 -      fi
    1.90 -      ;;
    1.91 -    o)
    1.92 -      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
    1.93 -      ;;
    1.94 -    q)
    1.95 -      TERMINATE=true
    1.96 -      ;;
    1.97 -    \?)
    1.98 -      usage
    1.99 -      ;;
   1.100 -  esac
   1.101 -done
   1.102 -
   1.103 -shift $(($OPTIND - 1))
   1.104 -
   1.105 -
   1.106 -# args
   1.107 -
   1.108 -HEAP=""
   1.109 -
   1.110 -if [ "$#" -ge 1 ]; then
   1.111 -  HEAP="$1"
   1.112 -  shift
   1.113 -fi
   1.114 -
   1.115 -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   1.116 -
   1.117 -
   1.118 -## check ML system
   1.119 -
   1.120 -[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   1.121 -
   1.122 -
   1.123 -## heap file
   1.124 -
   1.125 -declare -a FIRST_ML_OPTIONS=()
   1.126 -
   1.127 -[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"
   1.128 +isabelle_admin_build jars || exit $?
   1.129  
   1.130 -case "$HEAP" in
   1.131 -  RAW_ML_SYSTEM)
   1.132 -    HEAP_FILE=""
   1.133 -    ;;
   1.134 -  */*)
   1.135 -    HEAP_FILE="$HEAP"
   1.136 -    [ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\""
   1.137 -    ;;
   1.138 -  *)
   1.139 -    HEAP_FILE=""
   1.140 -    ISA_PATH=""
   1.141 -
   1.142 -    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
   1.143 -    for DIR in "${PATHS[@]}"
   1.144 -    do
   1.145 -      DIR="$DIR/$ML_IDENTIFIER"
   1.146 -      ISA_PATH="$ISA_PATH  $DIR\n"
   1.147 -      [ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP"
   1.148 -    done
   1.149 -
   1.150 -    if [ -z "$HEAP_FILE" ]; then
   1.151 -      echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2
   1.152 -      echo -ne "$ISA_PATH" >&2
   1.153 -      exit 2
   1.154 -    fi
   1.155 -    ;;
   1.156 -esac
   1.157 -
   1.158 -if [ -z "$HEAP_FILE" ]; then
   1.159 -  case "$ML_PLATFORM" in
   1.160 -    *-windows)
   1.161 -      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
   1.162 -      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
   1.163 -      ;;
   1.164 -    *)
   1.165 -      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
   1.166 -      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
   1.167 -      ;;
   1.168 -  esac
   1.169 -else
   1.170 -  check_file "$HEAP_FILE"
   1.171 -  case "$ML_PLATFORM" in
   1.172 -    *-windows)
   1.173 -      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
   1.174 -      ;;
   1.175 -    *)
   1.176 -      PLATFORM_HEAP_FILE="$HEAP_FILE"
   1.177 -      ;;
   1.178 -  esac
   1.179 -  PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")"
   1.180 -  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
   1.181 -  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)"
   1.182 -fi
   1.183 -
   1.184 -
   1.185 -## prepare tmp directory
   1.186 -
   1.187 -[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   1.188 -ISABELLE_PID="$$"
   1.189 -ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   1.190 -mkdir -p "$ISABELLE_TMP"
   1.191 -chmod $(umask -S) "$ISABELLE_TMP"
   1.192 -
   1.193 -
   1.194 -## ML text
   1.195 -
   1.196 -if [ -n "$MODES" ]; then
   1.197 -  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
   1.198 -  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Print_Mode.add_modes [$MODES]"
   1.199 -fi
   1.200 -
   1.201 -if [ -n "$SECURE" ]; then
   1.202 -  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
   1.203 -  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()"
   1.204 -fi
   1.205 -
   1.206 -if [ -n "$PROCESS_SOCKET" ]; then
   1.207 -  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
   1.208 -  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\""
   1.209 -else
   1.210 -  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   1.211 -  if [ -n "$OPTIONS_FILE" ]; then
   1.212 -    [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
   1.213 -      fail "Cannot provide options file and options on command-line"
   1.214 -    mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
   1.215 -      fail "Failed to move options file \"$OPTIONS_FILE\""
   1.216 -  else
   1.217 -    "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
   1.218 -      fail "Failed to retrieve Isabelle system options"
   1.219 -  fi
   1.220 -  if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
   1.221 -    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
   1.222 -    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()"
   1.223 -  fi
   1.224 -fi
   1.225 -
   1.226 -
   1.227 -## ML process
   1.228 -
   1.229 -check_file "$ML_HOME/poly"
   1.230 -librarypath "$ML_HOME"
   1.231 -
   1.232 -export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
   1.233 -
   1.234 -if [ -n "$TERMINATE" ]; then
   1.235 -  "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \
   1.236 -    "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null
   1.237 -  RC="$?"
   1.238 -else
   1.239 -  "$ISABELLE_HOME/lib/scripts/feeder" -p | \
   1.240 -    {
   1.241 -      read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
   1.242 -      RC="$?"
   1.243 -      kill -TERM "$FPID"
   1.244 -      exit "$RC"
   1.245 -    }
   1.246 -  RC="$?"
   1.247 -fi
   1.248 -
   1.249 -[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
   1.250 -rmdir "$ISABELLE_TMP"
   1.251 -
   1.252 -exit "$RC"
   1.253 +"$ISABELLE_TOOL" java isabelle.Isabelle_Process "$@"
     2.1 --- a/lib/scripts/feeder	Wed Mar 09 16:53:14 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,77 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Markus Wenzel, TU Muenchen
     2.7 -#
     2.8 -# feeder - feed isabelle session
     2.9 -
    2.10 -
    2.11 -## diagnostics
    2.12 -
    2.13 -PRG="$(basename "$0")"
    2.14 -DIR="$(dirname "$0")"
    2.15 -
    2.16 -function usage()
    2.17 -{
    2.18 -  echo
    2.19 -  echo "Usage: $PRG [OPTIONS]"
    2.20 -  echo
    2.21 -  echo "  Options are:"
    2.22 -  echo "    -h TEXT      head text (encoded as utf8)"
    2.23 -  echo "    -p           emit my pid"
    2.24 -  echo "    -q           do not pipe stdin"
    2.25 -  echo "    -t TEXT      tail text"
    2.26 -  echo
    2.27 -  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
    2.28 -  echo
    2.29 -  exit 1
    2.30 -}
    2.31 -
    2.32 -function fail()
    2.33 -{
    2.34 -  echo "$1" >&2
    2.35 -  exit 2
    2.36 -}
    2.37 -
    2.38 -
    2.39 -## process command line
    2.40 -
    2.41 -# options
    2.42 -
    2.43 -HEAD=""
    2.44 -EMITPID=""
    2.45 -QUIT=""
    2.46 -TAIL=""
    2.47 -
    2.48 -while getopts "h:pqt:" OPT
    2.49 -do
    2.50 -  case "$OPT" in
    2.51 -    h)
    2.52 -      HEAD="$OPTARG"
    2.53 -      ;;
    2.54 -    p)
    2.55 -      EMITPID=true
    2.56 -      ;;
    2.57 -    q)
    2.58 -      QUIT=true
    2.59 -      ;;
    2.60 -    t)
    2.61 -      TAIL="$OPTARG"
    2.62 -      ;;
    2.63 -    \?)
    2.64 -      usage
    2.65 -      ;;
    2.66 -  esac
    2.67 -done
    2.68 -
    2.69 -shift $(($OPTIND - 1))
    2.70 -
    2.71 -
    2.72 -# args
    2.73 -
    2.74 -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
    2.75 -
    2.76 -
    2.77 -
    2.78 -## main
    2.79 -
    2.80 -exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
     3.1 --- a/lib/scripts/feeder.pl	Wed Mar 09 16:53:14 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,47 +0,0 @@
     3.4 -#
     3.5 -# Author: Markus Wenzel, TU Muenchen
     3.6 -#
     3.7 -# feeder.pl - feed isabelle session
     3.8 -#
     3.9 -
    3.10 -# args
    3.11 -
    3.12 -($head, $emitpid, $quit, $tail) = @ARGV;
    3.13 -
    3.14 -
    3.15 -# setup signal handlers
    3.16 -
    3.17 -$SIG{'INT'} = "IGNORE";
    3.18 -
    3.19 -
    3.20 -# main
    3.21 -
    3.22 -#buffer lines
    3.23 -$| = 1;
    3.24 -
    3.25 -sub emit {
    3.26 -  my ($text) = @_;
    3.27 -  if ($text) {
    3.28 -    utf8::upgrade($text);
    3.29 -    $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
    3.30 -    print $text, "\n";
    3.31 -  }
    3.32 -}
    3.33 -
    3.34 -$emitpid && (print $$, "\n");
    3.35 -
    3.36 -emit("$head");
    3.37 -
    3.38 -if (!$quit) {
    3.39 -  while (<STDIN>) {
    3.40 -    print;
    3.41 -  }
    3.42 -}
    3.43 -
    3.44 -emit("$tail");
    3.45 -
    3.46 -
    3.47 -# wait forever
    3.48 -
    3.49 -close STDOUT;
    3.50 -sleep;
     4.1 --- a/src/Doc/System/Basics.thy	Wed Mar 09 16:53:14 2016 +0100
     4.2 +++ b/src/Doc/System/Basics.thy	Wed Mar 09 19:30:09 2016 +0100
     4.3 @@ -22,9 +22,7 @@
     4.4    to all Isabelle executables (including tools and user interfaces).
     4.5  
     4.6    \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
     4.7 -  logic sessions either interactively or in batch mode. In particular, this
     4.8 -  view abstracts over the invocation of the actual ML system to be used.
     4.9 -  Regular users rarely need to care about the low-level process.
    4.10 +  logic sessions in batch mode. This is rarely required for regular users.
    4.11  
    4.12    \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
    4.13    generic startup environment Isabelle related utilities, user interfaces etc.
    4.14 @@ -289,35 +287,25 @@
    4.15  section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
    4.16  
    4.17  text \<open>
    4.18 -  The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle
    4.19 -  logic sessions --- either interactively or in batch mode. It provides an
    4.20 -  abstraction over the underlying ML system and its saved heap files. Its
    4.21 -  usage is:
    4.22 +  The @{executable_def "isabelle_process"} executable runs a bare-bone
    4.23 +  Isabelle logic session in batch mode:
    4.24    @{verbatim [display]
    4.25  \<open>Usage: isabelle_process [OPTIONS] [HEAP]
    4.26  
    4.27    Options are:
    4.28 -    -O           system options from given YXML file
    4.29 -    -P SOCKET    startup process wrapper via TCP socket
    4.30 -    -S           secure mode -- disallow critical operations
    4.31      -e ML_EXPR   evaluate ML expression on startup
    4.32      -f ML_FILE   evaluate ML file on startup
    4.33      -m MODE      add print mode for output
    4.34      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    4.35 -    -q           non-interactive session
    4.36  
    4.37 -  If HEAP is a plain name (default "HOL"), it is searched in $ISABELLE_PATH;
    4.38 -  if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,
    4.39 -  the initial ML heap is used.\<close>}
    4.40 +  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
    4.41 +  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
    4.42 +  if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
    4.43  
    4.44 -  Heap files without path specifications are looked up in the @{setting
    4.45 -  ISABELLE_PATH} setting, which may consist of multiple components separated
    4.46 -  by colons --- these are tried in the given order with the value of @{setting
    4.47 -  ML_IDENTIFIER} appended internally. In a similar way, base names are
    4.48 -  relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any
    4.49 -  case, actual file locations may also be given by including at least one
    4.50 -  slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to refer to the current
    4.51 -  directory).
    4.52 +  Heap files without explicit directory specifications are looked up in the
    4.53 +  @{setting ISABELLE_PATH} setting, which may consist of multiple components
    4.54 +  separated by colons --- these are tried in the given order with the value of
    4.55 +  @{setting ML_IDENTIFIER} appended internally.
    4.56  \<close>
    4.57  
    4.58  
    4.59 @@ -331,45 +319,22 @@
    4.60  
    4.61    \<^medskip>
    4.62    The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
    4.63 -  session. Typically, this is used by some user interface, e.g.\ to enable
    4.64 -  output of proper mathematical symbols.
    4.65 -
    4.66 -  \<^medskip>
    4.67 -  Isabelle normally enters an interactive top-level loop (after processing the
    4.68 -  \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure
    4.69 -  batch mode facility.
    4.70 +  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
    4.71 +  mathematical Isabelle symbols.
    4.72  
    4.73    \<^medskip>
    4.74    Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
    4.75 -  see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies
    4.76 -  the full environment of system options as a file in YXML format (according
    4.77 -  to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>).
    4.78 -
    4.79 -  \<^medskip>
    4.80 -  The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper for Isabelle/Scala,
    4.81 -  with a private protocol running over the specified TCP socket. Isabelle/ML
    4.82 -  and Isabelle/Scala provide various programming interfaces to invoke protocol
    4.83 -  functions over untyped strings and XML trees.
    4.84 -
    4.85 -  \<^medskip>
    4.86 -  The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more secure by disabling some
    4.87 -  critical operations, notably runtime compilation and evaluation of ML source
    4.88 -  code.
    4.89 +  see also \secref{sec:system-options}.
    4.90  \<close>
    4.91  
    4.92  
    4.93  subsubsection \<open>Examples\<close>
    4.94  
    4.95  text \<open>
    4.96 -  Run an interactive session of the default object-logic (as specified by the
    4.97 -  @{setting ISABELLE_LOGIC} setting) like this:
    4.98 -  @{verbatim [display] \<open>isabelle_process\<close>}
    4.99 -
   4.100 -  \<^medskip>
   4.101 -  The next example demonstrates batch execution of Isabelle. We retrieve the
   4.102 -  \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
   4.103 -  quoting rules for the Bash shell vs.\ ML):
   4.104 -  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>}
   4.105 +  In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
   4.106 +  theory value from the theory loader within ML (observe the delicate quoting
   4.107 +  rules for the Bash shell vs.\ ML):
   4.108 +  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
   4.109  
   4.110    Note that the output text will be interspersed with additional junk messages
   4.111    by the ML runtime environment.
     5.1 --- a/src/HOL/Mirabelle/ex/Ex.thy	Wed Mar 09 16:53:14 2016 +0100
     5.2 +++ b/src/HOL/Mirabelle/ex/Ex.thy	Wed Mar 09 19:30:09 2016 +0100
     5.3 @@ -3,7 +3,7 @@
     5.4  
     5.5  ML {*
     5.6    val rc = Isabelle_System.bash
     5.7 -    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy";
     5.8 +    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle arith Inner_Product.thy";
     5.9    if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
    5.10    else ();
    5.11  *} -- "some arbitrary small test case"
     6.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Mar 09 16:53:14 2016 +0100
     6.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Mar 09 19:30:09 2016 +0100
     6.3 @@ -159,8 +159,7 @@
     6.4  
     6.5  my $cmd =
     6.6    "\"$ENV{'ISABELLE_PROCESS'}\" " .
     6.7 -  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\"' -q $mirabelle_logic" .
     6.8 -  $quiet;
     6.9 +  "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
    6.10  my $result = system "bash", "-c", $cmd;
    6.11  
    6.12  if ($output_log) {
     7.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Mar 09 16:53:14 2016 +0100
     7.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Mar 09 19:30:09 2016 +0100
     7.3 @@ -134,7 +134,7 @@
     7.4  # execution
     7.5  
     7.6  "$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
     7.7 -  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
     7.8 +  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
     7.9  
    7.10  
    7.11  [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
     8.1 --- a/src/HOL/TPTP/lib/Tools/tptp_graph	Wed Mar 09 16:53:14 2016 +0100
     8.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Wed Mar 09 19:30:09 2016 +0100
     8.3 @@ -118,7 +118,7 @@
     8.4  begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
     8.5  ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
     8.6          > $WORKDIR/$LOADER.thy
     8.7 -  "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" -q Pure
     8.8 +  "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" Pure
     8.9  }
    8.10  
    8.11  function cleanup_workdir()
     9.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Wed Mar 09 16:53:14 2016 +0100
     9.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Wed Mar 09 19:30:09 2016 +0100
     9.3 @@ -31,5 +31,5 @@
     9.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
     9.5  ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     9.6      > /tmp/$SCRATCH.thy
     9.7 -  "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
     9.8 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
     9.9  done
    10.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Wed Mar 09 16:53:14 2016 +0100
    10.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Wed Mar 09 19:30:09 2016 +0100
    10.3 @@ -31,5 +31,5 @@
    10.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    10.5  ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    10.6      > /tmp/$SCRATCH.thy
    10.7 -  "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    10.8 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    10.9  done
    11.1 --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Wed Mar 09 16:53:14 2016 +0100
    11.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Wed Mar 09 19:30:09 2016 +0100
    11.3 @@ -31,5 +31,5 @@
    11.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    11.5  ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    11.6      > /tmp/$SCRATCH.thy
    11.7 -  "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    11.8 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    11.9  done
    12.1 --- a/src/HOL/TPTP/lib/Tools/tptp_refute	Wed Mar 09 16:53:14 2016 +0100
    12.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Wed Mar 09 19:30:09 2016 +0100
    12.3 @@ -30,5 +30,5 @@
    12.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    12.5  ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    12.6      > /tmp/$SCRATCH.thy
    12.7 -  "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    12.8 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    12.9  done
    13.1 --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Wed Mar 09 16:53:14 2016 +0100
    13.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Wed Mar 09 19:30:09 2016 +0100
    13.3 @@ -31,5 +31,5 @@
    13.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    13.5  ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    13.6      > /tmp/$SCRATCH.thy
    13.7 -  "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    13.8 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    13.9  done
    14.1 --- a/src/HOL/TPTP/lib/Tools/tptp_translate	Wed Mar 09 16:53:14 2016 +0100
    14.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Wed Mar 09 19:30:09 2016 +0100
    14.3 @@ -28,4 +28,4 @@
    14.4  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    14.5  ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
    14.6    > /tmp/$SCRATCH.thy
    14.7 -"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    14.8 +"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    15.1 --- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 16:53:14 2016 +0100
    15.2 +++ b/src/Pure/Concurrent/bash.scala	Wed Mar 09 19:30:09 2016 +0100
    15.3 @@ -27,7 +27,9 @@
    15.4    }
    15.5  
    15.6    def process(script: String,
    15.7 -      cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process =
    15.8 +      cwd: JFile = null,
    15.9 +      env: Map[String, String] = Map.empty,
   15.10 +      redirect: Boolean = false): Process =
   15.11      new Process(script, cwd, env, redirect)
   15.12  
   15.13    class Process private [Bash](
    16.1 --- a/src/Pure/ROOT.ML	Wed Mar 09 16:53:14 2016 +0100
    16.2 +++ b/src/Pure/ROOT.ML	Wed Mar 09 19:30:09 2016 +0100
    16.3 @@ -83,8 +83,6 @@
    16.4  PolyML.Compiler.reportExhaustiveHandlers := true;
    16.5  PolyML.Compiler.printInAlphabeticalOrder := false;
    16.6  PolyML.Compiler.maxInlineSize := 80;
    16.7 -PolyML.Compiler.prompt1 := "ML> ";
    16.8 -PolyML.Compiler.prompt2 := "ML# ";
    16.9  
   16.10  fun ml_make_string struct_name =
   16.11    "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
    17.1 --- a/src/Pure/System/isabelle_system.scala	Wed Mar 09 16:53:14 2016 +0100
    17.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Mar 09 19:30:09 2016 +0100
    17.3 @@ -51,7 +51,7 @@
    17.4  
    17.5    @volatile private var _settings: Option[Map[String, String]] = None
    17.6  
    17.7 -  def settings(env: Map[String, String] = null): Map[String, String] =
    17.8 +  def settings(env: Map[String, String] = Map.empty): Map[String, String] =
    17.9    {
   17.10      if (_settings.isEmpty) init()  // unsynchronized check
   17.11      if (env == null) _settings.get else _settings.get ++ env
   17.12 @@ -302,7 +302,7 @@
   17.13  
   17.14    /* bash */
   17.15  
   17.16 -  def bash(script: String, cwd: JFile = null, env: Map[String, String] = null,
   17.17 +  def bash(script: String, cwd: JFile = null, env: Map[String, String] = Map.empty,
   17.18      progress_stdout: String => Unit = (_: String) => (),
   17.19      progress_stderr: String => Unit = (_: String) => (),
   17.20      progress_limit: Option[Long] = None,
    18.1 --- a/src/Pure/System/ml_process.scala	Wed Mar 09 16:53:14 2016 +0100
    18.2 +++ b/src/Pure/System/ml_process.scala	Wed Mar 09 19:30:09 2016 +0100
    18.3 @@ -7,6 +7,9 @@
    18.4  package isabelle
    18.5  
    18.6  
    18.7 +import java.io.{File => JFile}
    18.8 +
    18.9 +
   18.10  object ML_Process
   18.11  {
   18.12    def apply(options: Options,
   18.13 @@ -14,6 +17,8 @@
   18.14      args: List[String] = Nil,
   18.15      modes: List[String] = Nil,
   18.16      secure: Boolean = false,
   18.17 +    cwd: JFile = null,
   18.18 +    env: Map[String, String] = Map.empty,
   18.19      redirect: Boolean = false,
   18.20      channel: Option[System_Channel] = None): Bash.Process =
   18.21    {
   18.22 @@ -66,7 +71,7 @@
   18.23      // options
   18.24      val isabelle_process_options = Isabelle_System.tmp_file("options")
   18.25      File.write(isabelle_process_options, YXML.string_of_body(options.encode))
   18.26 -    val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
   18.27 +    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
   18.28      val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
   18.29  
   18.30      val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
   18.31 @@ -87,7 +92,7 @@
   18.32        (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
   18.33          map(eval => List("--eval", eval)).flatten ::: args
   18.34  
   18.35 -    Bash.process(env = env, redirect = redirect, script =
   18.36 +    Bash.process(
   18.37        """
   18.38          [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   18.39  
   18.40 @@ -104,6 +109,6 @@
   18.41          rmdir "$ISABELLE_TMP"
   18.42  
   18.43          exit "$RC"
   18.44 -      """)
   18.45 +      """, cwd = cwd, env = env ++ env_options, redirect = redirect)
   18.46    }
   18.47  }
    19.1 --- a/src/Pure/Tools/build.scala	Wed Mar 09 16:53:14 2016 +0100
    19.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 09 19:30:09 2016 +0100
    19.3 @@ -550,6 +550,7 @@
    19.4      catch { case ERROR(_) => /*error should be exposed in ML*/ }
    19.5  
    19.6      private val args_file = Isabelle_System.tmp_file("args")
    19.7 +    private val args_standard_path = File.standard_path(args_file)
    19.8      File.write(args_file, YXML.string_of_body(
    19.9        if (is_pure(name)) Options.encode(info.options)
   19.10        else
   19.11 @@ -566,48 +567,28 @@
   19.12              theories))))))))))))
   19.13          }))
   19.14  
   19.15 -    private val env =
   19.16 -    {
   19.17 -      val env0 =
   19.18 -        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
   19.19 -          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
   19.20 -            File.standard_path(args_file))
   19.21 -      if (is_pure(name))
   19.22 -        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
   19.23 -      else env0
   19.24 -    }
   19.25 +    output.file.delete
   19.26 +
   19.27 +    private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
   19.28  
   19.29 -    private val script =
   19.30 -      """
   19.31 -      . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   19.32 -      """ +
   19.33 -      (if (is_pure(name))
   19.34 -        """
   19.35 -          rm -f "$OUTPUT"
   19.36 -          "$ISABELLE_PROCESS" -f "ROOT.ML" \
   19.37 -            -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
   19.38 -            -q RAW_ML_SYSTEM
   19.39 -        """
   19.40 -      else
   19.41 -        """
   19.42 -        rm -f "$OUTPUT"
   19.43 -        "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
   19.44 -        """) +
   19.45 -      """
   19.46 -      RC="$?"
   19.47 -
   19.48 -      . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   19.49 -
   19.50 -      if [ "$RC" -eq 0 ]; then
   19.51 -        echo "Finished $TARGET ($TIMES_REPORT)" >&2
   19.52 -      fi
   19.53 -
   19.54 -      exit "$RC"
   19.55 -      """
   19.56 -
   19.57 -    private val future_result =
   19.58 +    private val future_result: Future[Process_Result] =
   19.59        Future.thread("build") {
   19.60 -        Isabelle_System.bash(script, info.dir.file, env,
   19.61 +        val process =
   19.62 +          if (is_pure(name)) {
   19.63 +            val eval =
   19.64 +              "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
   19.65 +              " Session.shutdown (); ML_Heap.share_common_data ();" +
   19.66 +              " ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));"
   19.67 +            val env1 = env + ("ISABELLE_PROCESS_OPTIONS" -> args_standard_path)
   19.68 +            ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
   19.69 +              cwd = info.dir.file, env = env1)
   19.70 +          }
   19.71 +          else {
   19.72 +            ML_Process(info.options, parent,
   19.73 +              List("--eval", "Build.build " + ML_Syntax.print_string_raw(args_standard_path)),
   19.74 +              cwd = info.dir.file, env = env)
   19.75 +          }
   19.76 +        process.result(
   19.77            progress_stdout = (line: String) =>
   19.78              Library.try_unprefix("\floading_theory = ", line) match {
   19.79                case Some(theory) => progress.theory(name, theory)
   19.80 @@ -876,7 +857,9 @@
   19.81              //{{{ finish job
   19.82  
   19.83              val process_result = job.join
   19.84 -            progress.echo(process_result.err)
   19.85 +            process_result.err_lines.foreach(progress.echo(_))
   19.86 +            if (process_result.ok)
   19.87 +              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   19.88  
   19.89              val process_result_tail =
   19.90              {
    20.1 --- a/src/Tools/Code/code_ml.ML	Wed Mar 09 16:53:14 2016 +0100
    20.2 +++ b/src/Tools/Code/code_ml.ML	Wed Mar 09 19:30:09 2016 +0100
    20.3 @@ -869,7 +869,7 @@
    20.4        check = { env_var = "ISABELLE_PROCESS",
    20.5          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    20.6          make_command = fn _ =>
    20.7 -          "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
    20.8 +          "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
    20.9    #> Code_Target.add_language
   20.10      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   20.11        check = { env_var = "ISABELLE_OCAML",