1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Oct 28 11:55:48 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Oct 28 17:43:43 2009 +0100
1.3 @@ -112,6 +112,13 @@
1.4 machine called \texttt{java}. The examples presented in this manual can be found
1.5 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
1.6
1.7 +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.8 +Nitpick also provides an automatic mode that can be enabled using the
1.9 +``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
1.10 +mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
1.11 +The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
1.12 +the ``Auto Counterexample Time Limit'' option.
1.13 +
1.14 \newbox\boxA
1.15 \setbox\boxA=\hbox{\texttt{nospam}}
1.16
1.17 @@ -154,16 +161,6 @@
1.18 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
1.19 available to Nitpick.
1.20
1.21 -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.22 -Nitpick also provides an automatic mode that can be enabled by specifying
1.23 -
1.24 -\prew
1.25 -\textbf{nitpick\_params} [\textit{auto}]
1.26 -\postw
1.27 -
1.28 -at the beginning of the theory file. In this mode, Nitpick is run for up to 5
1.29 -seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
1.30 -
1.31 \subsection{Propositional Logic}
1.32 \label{propositional-logic}
1.33
1.34 @@ -1595,6 +1592,17 @@
1.35 (\S\ref{authentication}), optimizations
1.36 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1.37
1.38 +You can instruct Nitpick to run automatically on newly entered theorems by
1.39 +enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
1.40 +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
1.41 +and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.42 +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.43 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.44 +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.45 +\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
1.46 +Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
1.47 +concise.
1.48 +
1.49 The number of options can be overwhelming at first glance. Do not let that worry
1.50 you: Nitpick's defaults have been chosen so that it almost always does the right
1.51 thing, and the most important options have been covered in context in
1.52 @@ -1622,35 +1630,19 @@
1.53 \end{enum}
1.54
1.55 Default values are indicated in square brackets. Boolean options have a negated
1.56 -counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
1.57 -options, ``= \textit{true}'' may be omitted.
1.58 +counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
1.59 +Boolean options, ``= \textit{true}'' may be omitted.
1.60
1.61 \subsection{Mode of Operation}
1.62 \label{mode-of-operation}
1.63
1.64 \begin{enum}
1.65 -\opfalse{auto}{no\_auto}
1.66 -Specifies whether Nitpick should be run automatically on newly entered theorems.
1.67 -For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
1.68 -\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.69 -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.70 -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.71 -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.72 -\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
1.73 -\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
1.74 -
1.75 -\nopagebreak
1.76 -{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
1.77 -
1.78 \optrue{blocking}{non\_blocking}
1.79 Specifies whether the \textbf{nitpick} command should operate synchronously.
1.80 The asynchronous (non-blocking) mode lets the user start proving the putative
1.81 theorem while Nitpick looks for a counterexample, but it can also be more
1.82 confusing. For technical reasons, automatic runs currently always block.
1.83
1.84 -\nopagebreak
1.85 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.86 -
1.87 \optrue{falsify}{satisfy}
1.88 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1.89 satisfying examples (models). This manual assumes throughout that
1.90 @@ -1670,16 +1662,15 @@
1.91 considered.
1.92
1.93 \nopagebreak
1.94 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
1.95 -(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
1.96 +{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
1.97 +(\S\ref{output-format}).}
1.98
1.99 \optrue{assms}{no\_assms}
1.100 Specifies whether the relevant assumptions in structured proof should be
1.101 considered. The option is implicitly enabled for automatic runs.
1.102
1.103 \nopagebreak
1.104 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.105 -and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.106 +{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.107
1.108 \opfalse{overlord}{no\_overlord}
1.109 Specifies whether Nitpick should put its temporary files in
1.110 @@ -1861,9 +1852,6 @@
1.111 option is useful to determine which scopes are tried or which SAT solver is
1.112 used. This option is implicitly disabled for automatic runs.
1.113
1.114 -\nopagebreak
1.115 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.116 -
1.117 \opfalse{debug}{no\_debug}
1.118 Specifies whether Nitpick should display additional debugging information beyond
1.119 what \textit{verbose} already displays. Enabling \textit{debug} also enables
1.120 @@ -1871,8 +1859,8 @@
1.121 option is implicitly disabled for automatic runs.
1.122
1.123 \nopagebreak
1.124 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
1.125 -(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
1.126 +{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
1.127 +\textit{batch\_size} (\S\ref{optimizations}).}
1.128
1.129 \optrue{show\_skolems}{hide\_skolem}
1.130 Specifies whether the values of Skolem constants should be displayed as part of
1.131 @@ -1910,8 +1898,7 @@
1.132 enabled.
1.133
1.134 \nopagebreak
1.135 -{\small See also \textit{auto} (\S\ref{mode-of-operation}),
1.136 -\textit{check\_potential} (\S\ref{authentication}), and
1.137 +{\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.138 \textit{sat\_solver} (\S\ref{optimizations}).}
1.139
1.140 \opt{max\_genuine}{int}{$\mathbf{1}$}
1.141 @@ -1968,8 +1955,7 @@
1.142 shown to be genuine, Nitpick displays a message to this effect and terminates.
1.143
1.144 \nopagebreak
1.145 -{\small See also \textit{max\_potential} (\S\ref{output-format}) and
1.146 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.147 +{\small See also \textit{max\_potential} (\S\ref{output-format}).}
1.148
1.149 \opfalse{check\_genuine}{trust\_genuine}
1.150 Specifies whether genuine and likely genuine counterexamples should be given to
1.151 @@ -1979,8 +1965,7 @@
1.152 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1.153
1.154 \nopagebreak
1.155 -{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
1.156 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.157 +{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
1.158
1.159 \ops{expect}{string}
1.160 Specifies the expected outcome, which must be one of the following:
1.161 @@ -2206,19 +2191,12 @@
1.162 Specifies the maximum amount of time that the \textbf{nitpick} command should
1.163 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.164 well as it can but offers no guarantees. For automatic runs,
1.165 -\textit{auto\_timeout} is used instead.
1.166 +\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
1.167 +a time slot whose length is specified by the ``Auto Counterexample Time
1.168 +Limit'' option in Proof General.
1.169
1.170 \nopagebreak
1.171 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.172 -and \textit{max\_threads} (\S\ref{optimizations}).}
1.173 -
1.174 -\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
1.175 -Specifies the maximum amount of time that Nitpick should use to find a
1.176 -counterexample when running automatically. Nitpick tries to honor this
1.177 -constraint as well as it can but offers no guarantees.
1.178 -
1.179 -\nopagebreak
1.180 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.181 +{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.182
1.183 \opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.184 Specifies the maximum amount of time that the \textit{auto} tactic should use