--- a/NEWS Fri Oct 02 21:29:09 2015 +0200
+++ b/NEWS Fri Oct 02 21:31:51 2015 +0200
@@ -249,9 +249,11 @@
- Handle Vampire 4.0 proof output without raising exception.
- Eliminated "MASH" environment variable. Use the "MaSh" option in
Isabelle/jEdit instead. INCOMPATIBILITY.
+ - Eliminated obsolete "blocking" option and related subcommands.
* Nitpick:
- Removed "check_potential" and "check_genuine" options.
+ - Eliminated obsolete "blocking" option.
* New commands lift_bnf and copy_bnf for lifting (copying) a BNF structure
on the raw type to an abstract type defined using typedef.
--- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 02 21:29:09 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 02 21:31:51 2015 +0200
@@ -345,9 +345,7 @@
\textit{compress} (\S\ref{output-format}).
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
-provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
-asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
-if you are the kind of user who can think clearly while ATPs are active.
+provers' time limit. It is set to 30 seconds by default.
\end{enum}
Options can be set globally using \textbf{sledgehammer\_params}
@@ -579,11 +577,6 @@
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
subgoal number \qty{num} (1 by default), with the given options and facts.
-\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
-by Sledgehammer. This allows you to examine results that might have been lost
-due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
-limit on the number of messages to display (10 by default).
-
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
automatic provers supported by Sledgehammer. See \S\ref{installation} and
\S\ref{mode-of-operation} for more information on how to install automatic
@@ -729,8 +722,8 @@
\end{enum}
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
-have a negative counterpart (e.g., \textit{blocking} vs.\
-\textit{non\_blocking}). When setting Boolean options or their negative
+have a negative counterpart (e.g., \textit{minimize} vs.\
+\textit{dont\_minimize}). When setting Boolean options or their negative
counterparts, ``= \textit{true\/}'' may be omitted.
\subsection{Mode of Operation}
@@ -920,14 +913,6 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opfalse{blocking}{non\_blocking}
-Specifies whether the \textbf{sledgehammer} command should operate
-synchronously. The asynchronous (non-blocking) mode lets the user start proving
-the putative theorem manually while Sledgehammer looks for a proof, but it can
-also be more confusing. Irrespective of the value of this option, Sledgehammer
-is always run synchronously if \textit{debug} (\S\ref{output-format}) is
-enabled.
-
\optrue{slice}{dont\_slice}
Specifies whether the time allocated to a prover should be sliced into several
segments, each of which has its own set of possibly prover-dependent options.
@@ -1235,8 +1220,7 @@
\opfalse{debug}{no\_debug}
Specifies whether Sledgehammer should display additional debugging information
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
-enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
-behind the scenes.
+enables \textit{verbose} behind the scenes.
\nopagebreak
{\small See also \textit{spy} (\S\ref{mode-of-operation}) and
@@ -1287,13 +1271,11 @@
problem.
\end{enum}
-Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
-(otherwise) if the actual outcome differs from the expected outcome. This option
-is useful for regression testing.
+Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is
+useful for regression testing.
\nopagebreak
-{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
-\textit{timeout} (\S\ref{timeouts}).}
+{\small See also \textit{timeout} (\S\ref{timeouts}).}
\end{enum}
\subsection{Timeouts}