# HG changeset patch # User wenzelm # Date 1457608310 -3600 # Node ID cd266473b81b55c46ab7177454828d144a2b4f8a # Parent e31bf8ed539778114bcb1d9d38e285124a778b64 isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual; diff -r e31bf8ed5397 -r cd266473b81b NEWS --- 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) diff -r e31bf8ed5397 -r cd266473b81b bin/isabelle_process --- 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 "$@" diff -r e31bf8ed5397 -r cd266473b81b lib/Tools/console --- 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 $? diff -r e31bf8ed5397 -r cd266473b81b lib/Tools/install --- 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" diff -r e31bf8ed5397 -r cd266473b81b lib/Tools/process --- /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 "$@" diff -r e31bf8ed5397 -r cd266473b81b lib/scripts/getsettings --- 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" diff -r e31bf8ed5397 -r cd266473b81b src/Doc/System/Basics.thy --- 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 \The Isabelle system environment\ text \ - This manual describes Isabelle together with related tools and user - interfaces as seen from a system oriented view. See also the \<^emph>\Isabelle/Isar - Reference Manual\ @{cite "isabelle-isar-ref"} for the actual Isabelle input - language and related concepts, and \<^emph>\The Isabelle/Isar Implementation - Manual\ @{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>\Isabelle settings\ mechanism provides process environment variables - to all Isabelle executables (including tools and user interfaces). - - \<^enum> The raw \<^emph>\Isabelle process\ (@{executable_ref "isabelle_process"}) runs - logic sessions in batch mode. This is rarely required for regular users. - - \<^enum> The main \<^emph>\Isabelle tool wrapper\ (@{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>\Isabelle/Isar Reference Manual\ @{cite + "isabelle-isar-ref"} for the actual Isabelle input language and related + concepts, and \<^emph>\The Isabelle/Isar Implementation Manual\ @{cite + "isabelle-implementation"} for the main concepts of the underlying + implementation in Isabelle/ML. \ section \Isabelle settings \label{sec:settings}\ text \ - The Isabelle system heavily depends on the \<^emph>\settings mechanism\. - Essentially, this is a statically scoped collection of environment + Isabelle executables may depend on the \<^emph>\Isabelle settings\ 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>\not\ intended to be set directly from the - shell, though. Isabelle employs a somewhat more sophisticated scheme of - \<^emph>\settings files\ --- 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>\components\ their \<^emph>\settings files\ as + explained below. \ @@ -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] \"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\} - \<^descr>[@{setting_def ISABELLE_PROCESS}\\<^sup>*\, @{setting ISABELLE_TOOL}\\<^sup>*\] 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}\\<^sup>*\] 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}\\<^sup>*\] refers to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2012\''. @@ -228,8 +201,8 @@ \<^verbatim>\dvi\ files. \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\\<^sup>*\] 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. \ @@ -284,13 +257,52 @@ \ -section \The raw Isabelle process \label{sec:isabelle-process}\ +section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ text \ - The @{executable_def "isabelle_process"} executable runs a bare-bone - Isabelle logic session in batch mode: + The main \<^emph>\Isabelle tool wrapper\ 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] -\Usage: isabelle_process [OPTIONS] [HEAP] +\Usage: isabelle TOOL [ARGS ...] + + Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. + +Available tools: + ...\} + + 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! +\ + + +subsubsection \Examples\ + +text \ + Show the list of available documentation of the Isabelle distribution: + @{verbatim [display] \isabelle doc\} + + View a certain document as follows: + @{verbatim [display] \isabelle doc system\} + + Query the Isabelle settings environment: + @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} +\ + + +section \The raw Isabelle ML process\ + +subsection \Batch mode \label{sec:tool-process}\ + +text \ + The @{tool_def process} tool runs the raw ML process in batch mode: + @{verbatim [display] +\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.\} Heap files without explicit directory specifications are looked up in the @@ -328,49 +342,60 @@ \ -subsubsection \Examples\ +subsubsection \Example\ text \ - In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\Main\ - theory value from the theory loader within ML (observe the delicate quoting - rules for the Bash shell vs.\ ML): - @{verbatim [display] \isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\} + The subsequent example retrieves the \<^verbatim>\Main\ theory value from the theory + loader within ML: + @{verbatim [display] \isabelle process -e 'Thy_Info.get_theory "Main"' HOL\} + + 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. \ -section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ +subsection \Interactive mode\ text \ - 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] -\Usage: isabelle TOOL [ARGS ...] +\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: - ...\} + Build a logic session image and run the raw Isabelle ML process + in interactive mode, with line editor ISABELLE_LINE_EDITOR.\} - 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! -\ + Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is + checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-r\ + abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap + Isabelle/Pure interactively. + Options \<^verbatim>\-d\ and \<^verbatim>\-s\ have the same meaning as for @{tool build} + (\secref{sec:tool-build}). + + Options \<^verbatim>\-m\ and \<^verbatim>\-o\ have the same meaning as for @{tool process} + (\secref{sec:tool-process}). -subsubsection \Examples\ - -text \ - Show the list of available documentation of the Isabelle distribution: - @{verbatim [display] \isabelle doc\} + \<^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] \isabelle doc system\} - - Query the Isabelle settings environment: - @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} + 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}. \ diff -r e31bf8ed5397 -r cd266473b81b src/Doc/System/Misc.thy --- 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 @@ \ -section \Raw ML console\ - -text \ - The @{tool_def console} tool runs the Isabelle process with raw ML console: - @{verbatim [display] -\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).\} - - Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is - checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-r\ - abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap - Isabelle/Pure interactively. - - Options \<^verbatim>\-d\ and \<^verbatim>\-s\ have the same meaning as for @{tool build} - (\secref{sec:tool-build}). - - Options \<^verbatim>\-m\ and \<^verbatim>\-o\ 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}. -\ - - section \Displaying documents \label{sec:tool-display}\ text \ @@ -213,7 +170,7 @@ determined by @{setting ISABELLE_HOME}. The \BINDIR\ 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>\$HOME/bin\. diff -r e31bf8ed5397 -r cd266473b81b src/Doc/System/Presentation.thy --- 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; \\ diff -r e31bf8ed5397 -r cd266473b81b src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- 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; diff -r e31bf8ed5397 -r cd266473b81b src/HOL/Mutabelle/lib/Tools/mutabelle --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/CASC/ReadMe --- 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. diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_graph --- 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() diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_isabelle --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_nitpick --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_refute --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- 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 diff -r e31bf8ed5397 -r cd266473b81b src/HOL/TPTP/lib/Tools/tptp_translate --- 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.$" diff -r e31bf8ed5397 -r cd266473b81b src/Pure/Tools/ml_console.scala --- 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), diff -r e31bf8ed5397 -r cd266473b81b src/Pure/Tools/ml_process.scala --- 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 => "" diff -r e31bf8ed5397 -r cd266473b81b src/Tools/Code/code_ml.ML --- 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",