doc-src/Nitpick/nitpick.tex

 
 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
 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}}
 
 The known bugs and limitations at the time of writing are listed in
 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick

 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
 be installed, as explained in \S\ref{optimizations}. If you have already
 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}
 
 Let's start with a trivial example from propositional logic:

 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
 format (\S\ref{output-format}), automatic counterexample checks
 (\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
 \S\ref{first-steps}.
 

 ``$f~x$''~``$g~y$'').
 \item[$\bullet$] \qtybf{type}: A HOL type.
 \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
 \textit{falsify} is enabled.

 these conditions are tagged as ``likely genuine.'' The \textit{debug}
 (\S\ref{output-format}) option can be used to find out which axioms were
 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
 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
 debugging Nitpick but also unsafe if several instances of the tool are run

 \opfalse{verbose}{quiet}
 Specifies whether the \textbf{nitpick} command should explain what it does. This
 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
 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
 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
 counterexamples. Skolem constants correspond to bound variables in the original
 formula and usually help us to understand why the counterexample falsifies the

 \textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
 identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
 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}$}
 Specifies the maximum number of genuine counterexamples to display. If you set
 this option to a value greater than 1, you will need an incremental SAT solver:

 Specifies whether potential counterexamples should be given to Isabelle's
 \textit{auto} tactic to assess their validity. If a potential counterexample is
 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
 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
 counterexample is shown to be spurious, the user is kindly asked to send a bug
 report to the author at
 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}[e-mail]}.
 
 \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:
 
 \begin{enum}

 \begin{enum}
 \opt{timeout}{time}{$\mathbf{30}$ s}
 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.
-
-\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}).}
+\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{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
 when checking a counterexample, and similarly that \textit{lexicographic\_order}
 and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive