# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 07ebc23987319edd5596312417fa377286778cee # Parent ade5c84f860f78c365d94307fdd3650e77ea37fa new timeout section (cf. Nitpick manual) diff -r ade5c84f860f -r 07ebc2398731 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200 @@ -343,11 +343,6 @@ and simply write the prover names as a space-separated list (e.g., ``\textit{e spass remote\_vampire}''). -\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) 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. - \item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding}) specifies whether type-sound encodings should be used. By default, Sledgehammer employs a mixture of type-sound and type-unsound encodings, occasionally @@ -364,6 +359,11 @@ that Isar proofs should be generated, instead of one-liner Metis proofs. The length of the Isar proofs can be controlled by setting \textit{isar\_shrink\_factor} (\S\ref{output-format}). + +\item[$\bullet$] \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. \end{enum} Options can be set globally using \textbf{sledgehammer\_params} @@ -514,7 +514,7 @@ Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds to ensure that the generated one-line proofs actually work and to display timing information. This can be configured using the \textit{preplay\_timeout} option -(\S\ref{mode-of-operation}).) +(\S\ref{timeouts}).) If you see the warning @@ -648,12 +648,11 @@ enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover, -\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{timeout} -(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in -Proof General's ``Isabelle'' menu, \textit{full\_types} -(\S\ref{problem-encoding}) is enabled, and \textit{verbose} -(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled. -Sledgehammer's output is also more concise. +\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{full\_types} +(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) +and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout} +(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof +General's ``Isabelle'' menu. Sledgehammer's output is also more concise. \section{Option Reference} \label{option-reference} @@ -678,7 +677,8 @@ Sledgehammer's options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), relevance filter (\S\ref{relevance-filter}), output format -(\S\ref{output-format}), and authentication (\S\ref{authentication}). +(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts +(\S\ref{timeouts}). The descriptions below refer to the following syntactic quantities: @@ -823,18 +823,6 @@ %\opnodefault{atp}{string} %Legacy alias for \textit{provers}. -\opdefault{timeout}{float\_or\_none}{\upshape 30} -Specifies the maximum number of seconds that the automatic provers should spend -searching for a proof. This excludes problem preparation and is a soft limit. -For historical reasons, the default value of this option can be overridden using -the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof -General. - -\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4} -Specifies the maximum number of seconds that Metis should be spent trying to -``preplay'' the found proof. If this option is set to 0, no preplaying takes -place, and no timing information is displayed next to the suggested Metis calls. - \opfalse{blocking}{non\_blocking} Specifies whether the \textbf{sledgehammer} command should operate synchronously. The asynchronous (non-blocking) mode lets the user start proving @@ -1049,7 +1037,6 @@ Specifies the granularity of the Isar proof. A value of $n$ indicates that each Isar proof step should correspond to a group of up to $n$ consecutive proof steps in the ATP proof. - \end{enum} \subsection{Authentication} @@ -1073,7 +1060,25 @@ is useful for regression testing. \nopagebreak -{\small See also \textit{blocking} (\S\ref{mode-of-operation}).} +{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and +\textit{timeout} (\S\ref{timeouts}).} +\end{enum} + +\subsection{Timeouts} +\label{timeouts} + +\begin{enum} +\opdefault{timeout}{float\_or\_none}{\upshape 30} +Specifies the maximum number of seconds that the automatic provers should spend +searching for a proof. This excludes problem preparation and is a soft limit. +For historical reasons, the default value of this option can be overridden using +the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof +General. + +\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4} +Specifies the maximum number of seconds that Metis should be spent trying to +``preplay'' the found proof. If this option is set to 0, no preplaying takes +place, and no timing information is displayed next to the suggested Metis calls. \end{enum} \let\em=\sl