isabelle_process is superseded by "isabelle process" tool;
tuned tool usage;
misc updates and tuning of "system" manual;
--- a/NEWS Thu Mar 10 12:11:23 2016 +0100
+++ b/NEWS Thu Mar 10 12:11:50 2016 +0100
@@ -218,6 +218,29 @@
*** System ***
+* SML/NJ and old versions of Poly/ML are no longer supported.
+
+* The executable "isabelle_process" has been discontinued. Tools and
+prover front-ends should use ML_Process or Isabelle_Process in
+Isabelle/Scala. Command-line usage works via "isabelle process" or
+"isabelle console". INCOMPATIBILITY.
+
+* The Isabelle system environment always ensures that the main
+executables are found within the shell search $PATH: "isabelle" and
+"isabelle_scala_script".
+
+* New command-line tool "isabelle process" supports ML evaluation of
+literal expressions (option -e) or files (option -f) in the context of a
+given heap image. Errors lead to premature exit of the ML process with
+return code 1.
+
+* Command-line tool "isabelle console" provides option -r to help to
+bootstrapping Isabelle/Pure interactively.
+
+* Command-line tool "isabelle yxml" has been discontinued.
+INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
+Isabelle/ML or Isabelle/Scala.
+
* File.bash_string, File.bash_path etc. represent Isabelle/ML and
Isabelle/Scala strings authentically within GNU bash. This is useful to
produce robust shell scripts under program control, without worrying
@@ -226,27 +249,6 @@
less versatile) operations File.shell_quote, File.shell_path etc. have
been discontinued.
-* The Isabelle system environment always ensures that the main
-executables are found within the PATH: isabelle, isabelle_process,
-isabelle_scala_script.
-
-* Command-line tool "isabelle_process" no longer supports writable heap
-images. INCOMPATIBILITY in exotic situations where "isabelle build"
-cannot be used: the structure ML_Heap provides operations to save the ML
-heap under program control.
-
-* Command-line tool "isabelle_process" supports ML evaluation of literal
-expressions (option -e) or files (option -f). Errors lead to premature
-exit of the ML process with return code 1.
-
-* Command-line tool "isabelle console -r" helps to bootstrap
-Isabelle/Pure interactively.
-
-* The somewhat pointless command-line tool "isabelle yxml" has been
-discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
-"YXML" in Isabelle/ML or Isabelle/Scala.
-
-* SML/NJ and old versions of Poly/ML are no longer supported.
New in Isabelle2016 (February 2016)
--- a/bin/isabelle_process Thu Mar 10 12:11:23 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Isabelle process startup script.
-
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-isabelle_admin_build jars || exit $?
-
-"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
--- a/lib/Tools/console Thu Mar 10 12:11:23 2016 +0100
+++ b/lib/Tools/console Thu Mar 10 12:11:50 2016 +0100
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# DESCRIPTION: run Isabelle process with raw ML console and line editor
+# DESCRIPTION: raw ML process (interactive mode)
isabelle_admin_build jars || exit $?
--- a/lib/Tools/install Thu Mar 10 12:11:23 2016 +0100
+++ b/lib/Tools/install Thu Mar 10 12:11:50 2016 +0100
@@ -63,7 +63,7 @@
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
-for NAME in isabelle isabelle_process isabelle_scala_script
+for NAME in isabelle isabelle_scala_script
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/process Thu Mar 10 12:11:50 2016 +0100
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: raw ML process (batch mode)
+
+isabelle_admin_build jars || exit $?
+
+case "$ISABELLE_JAVA_PLATFORM" in
+ x86-*)
+ ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
+ ;;
+ x86_64-*)
+ ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
+ ;;
+esac
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+
+mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
+
+"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
--- a/lib/scripts/getsettings Thu Mar 10 12:11:23 2016 +0100
+++ b/lib/scripts/getsettings Thu Mar 10 12:11:50 2016 +0100
@@ -55,7 +55,6 @@
#main executables
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
PATH="$ISABELLE_HOME/bin:$PATH"
--- a/src/Doc/System/Basics.thy Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Doc/System/Basics.thy Thu Mar 10 12:11:50 2016 +0100
@@ -7,49 +7,24 @@
chapter \<open>The Isabelle system environment\<close>
text \<open>
- This manual describes Isabelle together with related tools and user
- interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar
- Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input
- language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation
- Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the
- underlying implementation in Isabelle/ML.
-
- \<^medskip>
- The Isabelle system environment provides the following basic infrastructure
- to integrate tools smoothly.
-
- \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables
- to all Isabelle executables (including tools and user interfaces).
-
- \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
- logic sessions in batch mode. This is rarely required for regular users.
-
- \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
- generic startup environment Isabelle related utilities, user interfaces etc.
- Such tools automatically benefit from the settings mechanism.
+ This manual describes Isabelle together with related tools as seen from a
+ system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
+ "isabelle-isar-ref"} for the actual Isabelle input language and related
+ concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
+ "isabelle-implementation"} for the main concepts of the underlying
+ implementation in Isabelle/ML.
\<close>
section \<open>Isabelle settings \label{sec:settings}\<close>
text \<open>
- The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>.
- Essentially, this is a statically scoped collection of environment
+ Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
+ process environment. This is a statically scoped collection of environment
variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
- shell, though. Isabelle employs a somewhat more sophisticated scheme of
- \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional
- user-specific modifications. With all configuration variables in clearly
- defined places, this scheme is more maintainable and user-friendly than
- global shell environment variables.
-
- In particular, we avoid the typical situation where prospective users of a
- software package are told to put several things into their shell startup
- scripts, before being able to actually run the program. Isabelle requires
- none such administrative chores of its end-users --- the executables can be
- invoked straight away. Occasionally, users would still want to put the
- @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but
- this is not required.
+ shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
+ explained below.
\<close>
@@ -101,9 +76,8 @@
\<^medskip>
A few variables are somewhat special:
- \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
- automatically to the absolute path names of the @{executable
- "isabelle_process"} and @{executable isabelle} executables, respectively.
+ \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
+ name of the @{executable isabelle} executables.
\<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
@@ -162,11 +136,10 @@
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
- \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are
- automatically set to the full path names of the @{executable
- "isabelle_process"} and @{executable isabelle} executables, respectively.
- Thus other tools and scripts need not assume that the @{file
- "$ISABELLE_HOME/bin"} directory is on the current search path of the shell.
+ \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
+ of the @{executable isabelle} executable. Thus other tools and scripts need
+ not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
+ search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
@@ -228,8 +201,8 @@
\<^verbatim>\<open>dvi\<close> files.
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
- running @{executable "isabelle_process"} derives an individual directory for
- temporary files.
+ running Isabelle ML process derives an individual directory for temporary
+ files.
\<close>
@@ -284,13 +257,52 @@
\<close>
-section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
+section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
text \<open>
- The @{executable_def "isabelle_process"} executable runs a bare-bone
- Isabelle logic session in batch mode:
+ The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
+ Isabelle related utilities, user interfaces etc. Such tools automatically
+ benefit from the settings mechanism. All Isabelle command-line tools are
+ invoked via a common wrapper --- @{executable_ref isabelle}:
@{verbatim [display]
-\<open>Usage: isabelle_process [OPTIONS] [HEAP]
+\<open>Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+
+Available tools:
+ ...\<close>}
+
+ In principle, Isabelle tools are ordinary executable scripts that are run
+ within the Isabelle settings environment, see \secref{sec:settings}. The set
+ of available tools is collected by @{executable isabelle} from the
+ directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
+ call the scripts directly from the shell. Neither should you add the tool
+ directories to your shell's search path!
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Show the list of available documentation of the Isabelle distribution:
+ @{verbatim [display] \<open>isabelle doc\<close>}
+
+ View a certain document as follows:
+ @{verbatim [display] \<open>isabelle doc system\<close>}
+
+ Query the Isabelle settings environment:
+ @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
+\<close>
+
+
+section \<open>The raw Isabelle ML process\<close>
+
+subsection \<open>Batch mode \label{sec:tool-process}\<close>
+
+text \<open>
+ The @{tool_def process} tool runs the raw ML process in batch mode:
+ @{verbatim [display]
+\<open>Usage: isabelle process [OPTIONS] [HEAP]
Options are:
-e ML_EXPR evaluate ML expression on startup
@@ -298,8 +310,10 @@
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
- $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+ Run the raw Isabelle ML process in batch mode, using a given heap image.
+
+ If HEAP is a plain name (default ISABELLE_LOGIC), it is searched in
+ ISABELLE_PATH; if it contains a slash, it is taken as literal file;
if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
Heap files without explicit directory specifications are looked up in the
@@ -328,49 +342,60 @@
\<close>
-subsubsection \<open>Examples\<close>
+subsubsection \<open>Example\<close>
text \<open>
- In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
- theory value from the theory loader within ML (observe the delicate quoting
- rules for the Bash shell vs.\ ML):
- @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
+ The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
+ loader within ML:
+ @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
+
+ Observe the delicate quoting rules for the Bash shell vs.\ ML. The
+ Isabelle/ML and Scala libraries provide functions for that, but here we need
+ to do it manually.
\<close>
-section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
+subsection \<open>Interactive mode\<close>
text \<open>
- All Isabelle related tools and interfaces are called via a common wrapper
- --- @{executable isabelle}:
+ The @{tool_def console} tool runs the raw ML process with interactive
+ console and line editor:
@{verbatim [display]
-\<open>Usage: isabelle TOOL [ARGS ...]
+\<open>Usage: isabelle console [OPTIONS]
- Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC)
+ -m MODE add print mode for output
+ -n no build of session image on startup
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -r logic session is RAW_ML_SYSTEM
+ -s system build mode for session image
-Available tools:
- ...\<close>}
+ Build a logic session image and run the raw Isabelle ML process
+ in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
- In principle, Isabelle tools are ordinary executable scripts that are run
- within the Isabelle settings environment, see \secref{sec:settings}. The set
- of available tools is collected by @{executable isabelle} from the
- directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
- call the scripts directly from the shell. Neither should you add the tool
- directories to your shell's search path!
-\<close>
+ Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
+ checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
+ abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+ Isabelle/Pure interactively.
+ Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
+ (\secref{sec:tool-build}).
+
+ Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
+ (\secref{sec:tool-process}).
-subsubsection \<open>Examples\<close>
-
-text \<open>
- Show the list of available documentation of the Isabelle distribution:
- @{verbatim [display] \<open>isabelle doc\<close>}
+ \<^medskip>
+ The Isabelle/ML process is run through the line editor that is specified via
+ the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
+ @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
+ standard input/output.
- View a certain document as follows:
- @{verbatim [display] \<open>isabelle doc system\<close>}
-
- Query the Isabelle settings environment:
- @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
+ The user is connected to the raw ML toplevel loop: this is neither
+ Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
+ relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
+ use_thys}.
\<close>
--- a/src/Doc/System/Misc.thy Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Doc/System/Misc.thy Thu Mar 10 12:11:50 2016 +0100
@@ -56,49 +56,6 @@
\<close>
-section \<open>Raw ML console\<close>
-
-text \<open>
- The @{tool_def console} tool runs the Isabelle process with raw ML console:
- @{verbatim [display]
-\<open>Usage: isabelle console [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -n no build of session image on startup
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
- -s system build mode for session image
-
- Run Isabelle process with raw ML console and line editor
- (default ISABELLE_LINE_EDITOR).\<close>}
-
- Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
- checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
- abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
- Isabelle/Pure interactively.
-
- Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
- (\secref{sec:tool-build}).
-
- Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
- isabelle_process} (\secref{sec:isabelle-process}).
-
- \<^medskip>
- The Isabelle/ML process is run through the line editor that is specified via
- the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
- @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
- standard input/output.
-
- The user is connected to the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
- relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
- use_thys}.
-\<close>
-
-
section \<open>Displaying documents \label{sec:tool-display}\<close>
text \<open>
@@ -213,7 +170,7 @@
determined by @{setting ISABELLE_HOME}.
The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
- @{executable "isabelle_process"} and @{executable isabelle} should be
+ @{executable "isabelle"} and @{executable isabelle_scala_script} should be
placed, which is typically a directory in the shell's @{setting PATH}, such
as \<^verbatim>\<open>$HOME/bin\<close>.
--- a/src/Doc/System/Presentation.thy Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Doc/System/Presentation.thy Thu Mar 10 12:11:50 2016 +0100
@@ -17,11 +17,10 @@
The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
for managing Isabelle sessions, including proper setup for presentation;
- @{tool build} takes care to have @{executable_ref "isabelle_process"} run
- any additional stages required for document preparation, notably the
- @{tool_ref document} and @{tool_ref latex}. The complete tool chain for
- managing batch-mode Isabelle sessions is illustrated in
- \figref{fig:session-tools}.
+ @{tool build} tells the Isabelle process to run any additional stages
+ required for document preparation, notably the @{tool_ref document} and
+ @{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle
+ sessions is illustrated in \figref{fig:session-tools}.
\begin{figure}[htbp]
\begin{center}
@@ -34,8 +33,7 @@
@{tool_ref build} & invoked repeatedly by the user to keep
session output up-to-date (HTML, documents etc.); \\
- @{executable "isabelle_process"} & run through @{tool_ref
- build}; \\
+ @{tool_ref process} & run through @{tool_ref build}; \\
@{tool_ref document} & run by the Isabelle process if document
preparation is enabled; \\
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 12:11:50 2016 +0100
@@ -158,7 +158,7 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $cmd =
- "\"$ENV{'ISABELLE_PROCESS'}\" " .
+ "\"$ENV{'ISABELLE_TOOL'}\" process " .
"-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 12:11:50 2016 +0100
@@ -133,7 +133,7 @@
# execution
-"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
+"$ISABELLE_TOOL" process -o auto_time_limit=10.0 \
-e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
--- a/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 12:11:50 2016 +0100
@@ -180,7 +180,7 @@
Then I ran
- ./bin/isabelle_process -e 'use_thy "/tmp/T";'
+ ./bin/isabelle process -e 'use_thy "/tmp/T";'
I also performed the aforementioned sanity tests.
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 12:11:50 2016 +0100
@@ -118,7 +118,7 @@
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
- "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+ "$ISABELLE_TOOL" process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
}
function cleanup_workdir()
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 12:11:50 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$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.$"
+ "$ISABELLE_TOOL" 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.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 12:11:50 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$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.$"
+ "$ISABELLE_TOOL" 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.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 12:11:50 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$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.$"
+ "$ISABELLE_TOOL" 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.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 12:11:50 2016 +0100
@@ -30,5 +30,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$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.$"
+ "$ISABELLE_TOOL" 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.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 12:11:50 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$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.$"
+ "$ISABELLE_TOOL" 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.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 12:11:23 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 12:11:50 2016 +0100
@@ -28,4 +28,4 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-"$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.$"
+"$ISABELLE_TOOL" 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.$"
--- a/src/Pure/Tools/ml_console.scala Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Thu Mar 10 12:11:50 2016 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/ml_console.scala
Author: Makarius
-The raw ML process with interaction (line editor).
+The raw ML process in interactive mode.
*/
package isabelle
@@ -33,11 +33,12 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
+ -r logic session is "RAW_ML_SYSTEM"
-s system build mode for session image
- Run Isabelle process with raw ML console and line editor
- (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
+ Build a logic session image and run the raw Isabelle ML process
+ in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
+ quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg),
--- a/src/Pure/Tools/ml_process.scala Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Thu Mar 10 12:11:50 2016 +0100
@@ -36,7 +36,7 @@
dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
case Some(heap_path) => List(heap_path)
case None =>
- error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
+ error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
cat_lines(dirs.map(dir => " " + dir.implode)))
}
}
@@ -124,7 +124,7 @@
var options = Options.init()
val getopts = Getopts("""
-Usage: isabelle_process [OPTIONS] [HEAP]
+Usage: isabelle process [OPTIONS] [HEAP]
Options are:
-e ML_EXPR evaluate ML expression on startup
@@ -132,15 +132,19 @@
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
- $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
- if it is RAW_ML_SYSTEM, the initial ML heap is used.
+ Run the raw Isabelle ML process in batch mode, using a given heap image.
+
+ If HEAP is a plain name (default ISABELLE_LOGIC=""" +
+ quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
+ ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+ if it is "RAW_ML_SYSTEM", the initial ML heap is used.
""",
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
"m:" -> (arg => modes = arg :: modes),
"o:" -> (arg => options = options + arg))
+ if (args.isEmpty) getopts.usage()
val heap =
getopts(args) match {
case Nil => ""
--- a/src/Tools/Code/code_ml.ML Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Tools/Code/code_ml.ML Thu Mar 10 12:11:50 2016 +0100
@@ -868,10 +868,10 @@
val _ = Theory.setup
(Code_Target.add_language
(target_SML, { serializer = serializer_sml, literals = literals_sml,
- check = { env_var = "ISABELLE_PROCESS",
+ check = { env_var = "ISABELLE_TOOL",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
+ "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
#> Code_Target.add_language
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",