--- 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