1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
1.3 @@ -343,11 +343,6 @@
1.4 and simply write the prover names as a space-separated list (e.g., ``\textit{e
1.5 spass remote\_vampire}'').
1.6
1.7 -\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) controls
1.8 -the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
1.9 -asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
1.10 -if you are the kind of user who can think clearly while ATPs are active.
1.11 -
1.12 \item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
1.13 specifies whether type-sound encodings should be used. By default, Sledgehammer
1.14 employs a mixture of type-sound and type-unsound encodings, occasionally
1.15 @@ -364,6 +359,11 @@
1.16 that Isar proofs should be generated, instead of one-liner Metis proofs. The
1.17 length of the Isar proofs can be controlled by setting
1.18 \textit{isar\_shrink\_factor} (\S\ref{output-format}).
1.19 +
1.20 +\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
1.21 +provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
1.22 +asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
1.23 +if you are the kind of user who can think clearly while ATPs are active.
1.24 \end{enum}
1.25
1.26 Options can be set globally using \textbf{sledgehammer\_params}
1.27 @@ -514,7 +514,7 @@
1.28 Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
1.29 to ensure that the generated one-line proofs actually work and to display timing
1.30 information. This can be configured using the \textit{preplay\_timeout} option
1.31 -(\S\ref{mode-of-operation}).)
1.32 +(\S\ref{timeouts}).)
1.33
1.34 If you see the warning
1.35
1.36 @@ -648,12 +648,11 @@
1.37 enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
1.38 General. For automatic runs, only the first prover set using \textit{provers}
1.39 (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
1.40 -\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{timeout}
1.41 -(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
1.42 -Proof General's ``Isabelle'' menu, \textit{full\_types}
1.43 -(\S\ref{problem-encoding}) is enabled, and \textit{verbose}
1.44 -(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled.
1.45 -Sledgehammer's output is also more concise.
1.46 +\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{full\_types}
1.47 +(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
1.48 +and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
1.49 +(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
1.50 +General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
1.51
1.52 \section{Option Reference}
1.53 \label{option-reference}
1.54 @@ -678,7 +677,8 @@
1.55 Sledgehammer's options are categorized as follows:\ mode of operation
1.56 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
1.57 relevance filter (\S\ref{relevance-filter}), output format
1.58 -(\S\ref{output-format}), and authentication (\S\ref{authentication}).
1.59 +(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
1.60 +(\S\ref{timeouts}).
1.61
1.62 The descriptions below refer to the following syntactic quantities:
1.63
1.64 @@ -823,18 +823,6 @@
1.65 %\opnodefault{atp}{string}
1.66 %Legacy alias for \textit{provers}.
1.67
1.68 -\opdefault{timeout}{float\_or\_none}{\upshape 30}
1.69 -Specifies the maximum number of seconds that the automatic provers should spend
1.70 -searching for a proof. This excludes problem preparation and is a soft limit.
1.71 -For historical reasons, the default value of this option can be overridden using
1.72 -the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
1.73 -General.
1.74 -
1.75 -\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
1.76 -Specifies the maximum number of seconds that Metis should be spent trying to
1.77 -``preplay'' the found proof. If this option is set to 0, no preplaying takes
1.78 -place, and no timing information is displayed next to the suggested Metis calls.
1.79 -
1.80 \opfalse{blocking}{non\_blocking}
1.81 Specifies whether the \textbf{sledgehammer} command should operate
1.82 synchronously. The asynchronous (non-blocking) mode lets the user start proving
1.83 @@ -1049,7 +1037,6 @@
1.84 Specifies the granularity of the Isar proof. A value of $n$ indicates that each
1.85 Isar proof step should correspond to a group of up to $n$ consecutive proof
1.86 steps in the ATP proof.
1.87 -
1.88 \end{enum}
1.89
1.90 \subsection{Authentication}
1.91 @@ -1073,7 +1060,25 @@
1.92 is useful for regression testing.
1.93
1.94 \nopagebreak
1.95 -{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
1.96 +{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
1.97 +\textit{timeout} (\S\ref{timeouts}).}
1.98 +\end{enum}
1.99 +
1.100 +\subsection{Timeouts}
1.101 +\label{timeouts}
1.102 +
1.103 +\begin{enum}
1.104 +\opdefault{timeout}{float\_or\_none}{\upshape 30}
1.105 +Specifies the maximum number of seconds that the automatic provers should spend
1.106 +searching for a proof. This excludes problem preparation and is a soft limit.
1.107 +For historical reasons, the default value of this option can be overridden using
1.108 +the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
1.109 +General.
1.110 +
1.111 +\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
1.112 +Specifies the maximum number of seconds that Metis should be spent trying to
1.113 +``preplay'' the found proof. If this option is set to 0, no preplaying takes
1.114 +place, and no timing information is displayed next to the suggested Metis calls.
1.115 \end{enum}
1.116
1.117 \let\em=\sl