doc-src/Nitpick/nitpick.tex
changeset 33561 ab01b72715ef
parent 33559 63925777ccf9
child 33564 75ce0f60617a
--- a/doc-src/Nitpick/nitpick.tex	Wed Oct 28 11:55:48 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Oct 28 17:43:43 2009 +0100
@@ -112,6 +112,13 @@
 machine called \texttt{java}. The examples presented in this manual can be found
 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
 
+Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
+Nitpick also provides an automatic mode that can be enabled using the
+``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
+mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
+The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
+the ``Auto Counterexample Time Limit'' option.
+
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
@@ -154,16 +161,6 @@
 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
 available to Nitpick.
 
-Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
-Nitpick also provides an automatic mode that can be enabled by specifying
-
-\prew
-\textbf{nitpick\_params} [\textit{auto}]
-\postw
-
-at the beginning of the theory file. In this mode, Nitpick is run for up to 5
-seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
-
 \subsection{Propositional Logic}
 \label{propositional-logic}
 
@@ -1595,6 +1592,17 @@
 (\S\ref{authentication}), optimizations
 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
 
+You can instruct Nitpick to run automatically on newly entered theorems by
+enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
+General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
+and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
+\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
+disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
+\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
+Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
+concise.
+
 The number of options can be overwhelming at first glance. Do not let that worry
 you: Nitpick's defaults have been chosen so that it almost always does the right
 thing, and the most important options have been covered in context in
@@ -1622,35 +1630,19 @@
 \end{enum}
 
 Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
-options, ``= \textit{true}'' may be omitted.
+counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
+Boolean options, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
 
 \begin{enum}
-\opfalse{auto}{no\_auto}
-Specifies whether Nitpick should be run automatically on newly entered theorems.
-For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
-\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
-\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
-(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
-disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
-\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
-\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
-
-\nopagebreak
-{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
-
 \optrue{blocking}{non\_blocking}
 Specifies whether the \textbf{nitpick} command should operate synchronously.
 The asynchronous (non-blocking) mode lets the user start proving the putative
 theorem while Nitpick looks for a counterexample, but it can also be more
 confusing. For technical reasons, automatic runs currently always block.
 
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
 \optrue{falsify}{satisfy}
 Specifies whether Nitpick should look for falsifying examples (countermodels) or
 satisfying examples (models). This manual assumes throughout that
@@ -1670,16 +1662,15 @@
 considered.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
-(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
+{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
+(\S\ref{output-format}).}
 
 \optrue{assms}{no\_assms}
 Specifies whether the relevant assumptions in structured proof should be
 considered. The option is implicitly enabled for automatic runs.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
+{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
 
 \opfalse{overlord}{no\_overlord}
 Specifies whether Nitpick should put its temporary files in
@@ -1861,9 +1852,6 @@
 option is useful to determine which scopes are tried or which SAT solver is
 used. This option is implicitly disabled for automatic runs.
 
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
 \opfalse{debug}{no\_debug}
 Specifies whether Nitpick should display additional debugging information beyond
 what \textit{verbose} already displays. Enabling \textit{debug} also enables
@@ -1871,8 +1859,8 @@
 option is implicitly disabled for automatic runs.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
-(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
+{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
+\textit{batch\_size} (\S\ref{optimizations}).}
 
 \optrue{show\_skolems}{hide\_skolem}
 Specifies whether the values of Skolem constants should be displayed as part of
@@ -1910,8 +1898,7 @@
 enabled.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}),
-\textit{check\_potential} (\S\ref{authentication}), and
+{\small See also \textit{check\_potential} (\S\ref{authentication}) and
 \textit{sat\_solver} (\S\ref{optimizations}).}
 
 \opt{max\_genuine}{int}{$\mathbf{1}$}
@@ -1968,8 +1955,7 @@
 shown to be genuine, Nitpick displays a message to this effect and terminates.
 
 \nopagebreak
-{\small See also \textit{max\_potential} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_potential} (\S\ref{output-format}).}
 
 \opfalse{check\_genuine}{trust\_genuine}
 Specifies whether genuine and likely genuine counterexamples should be given to
@@ -1979,8 +1965,7 @@
 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
 
 \nopagebreak
-{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
 
 \ops{expect}{string}
 Specifies the expected outcome, which must be one of the following:
@@ -2206,19 +2191,12 @@
 Specifies the maximum amount of time that the \textbf{nitpick} command should
 spend looking for a counterexample. Nitpick tries to honor this constraint as
 well as it can but offers no guarantees. For automatic runs,
-\textit{auto\_timeout} is used instead.
+\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
+a time slot whose length is specified by the ``Auto Counterexample Time
+Limit'' option in Proof General.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{max\_threads} (\S\ref{optimizations}).}
-
-\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
-Specifies the maximum amount of time that Nitpick should use to find a
-counterexample when running automatically. Nitpick tries to honor this
-constraint as well as it can but offers no guarantees.
-
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
+{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
 
 \opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
 Specifies the maximum amount of time that the \textit{auto} tactic should use