# HG changeset patch # User blanchet # Date 1379709570 -7200 # Node ID cf37f4b84824c284720402994e5255bc4660cce2 # Parent a198ce71de119635cd0c56bad472b29429a08d6e moved focus to Isabell/jEdit and away from Proof General diff -r a198ce71de11 -r cf37f4b84824 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Fri Sep 20 22:39:30 2013 +0200 +++ b/src/Doc/Nitpick/document/root.tex Fri Sep 20 22:39:30 2013 +0200 @@ -114,16 +114,9 @@ must find a model for the axioms. If it finds no model, we have an indication that the axioms might be unsatisfiable. -You can also invoke Nitpick from the ``Commands'' submenu of the -``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a -C-n. This is equivalent to entering the \textbf{nitpick} command with no -arguments in the theory text. - -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. -Nitpick also provides an automatic mode that can be enabled via the ``Auto -Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode, -Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick -and other automatic tools can be set using the ``Auto Tools Time Limit'' option. +For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled +via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle > +General.'' In this mode, Nitpick is run on every newly entered theorem. \newbox\boxA \setbox\boxA=\hbox{\texttt{nospam}} @@ -148,7 +141,7 @@ \section{Installation} \label{installation} -Sledgehammer is part of Isabelle, so you don't need to install it. However, it +Nitpick is part of Isabelle, so you don't need to install it. However, it relies on a third-party Kodkod front-end called Kodkodi as well as a Java virtual machine called \texttt{java} (version 1.5 or above). @@ -1874,17 +1867,18 @@ (\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}), +If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can +be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options +> Isabelle > General.'' For automatic runs, +\textit{user\_axioms} (\S\ref{mode-of-operation}), \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono} (\S\ref{scope-of-search}) 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\_threads} (\S\ref{optimizations}) is taken to be 1, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and \textit{timeout} -(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in -Proof General's ``Isabelle'' menu. Nitpick's output is also more concise. +(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. 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 @@ -2523,10 +2517,9 @@ \opdefault{timeout}{float\_or\_none}{\upshape 30} Specifies the maximum number of seconds 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{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. +well as it can but offers no guarantees. For automatic runs, the ``Auto Time +Limit'' option under ``Plugins > Plugin Options > Isabelle > General'' is used +instead. \nopagebreak {\small See also \textit{max\_threads} (\S\ref{optimizations}).} diff -r a198ce71de11 -r cf37f4b84824 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Sep 20 22:39:30 2013 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Fri Sep 20 22:39:30 2013 +0200 @@ -112,11 +112,6 @@ The problem passed to the automatic provers consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the current theory context, filtered by relevance. -%Because jobs are run in the -%background, you can continue to work on your proof by other means. Provers can -%be run in parallel. -%Any reply (which may arrive half a minute later) will appear -%in the Proof General response buffer. The result of a successful proof search is some source text that usually (but not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed @@ -124,12 +119,10 @@ integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. -In this manual, we will explicitly invoke the \textbf{sledgehammer} command. -For Proof General users, Sledgehammer also provides an automatic mode that can -be enabled via the ``Auto Sledgehammer'' option in the ``Isabelle'' menu. In -this mode, Sledgehammer is run on every newly entered theorem. The time limit -for Auto Sledgehammer and other automatic tools can be set using the ``Auto -Tools Time Limit'' option. +For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be +enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > +Isabelle > General.'' In this mode, Sledgehammer is run on every newly entered +theorem. \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} @@ -268,11 +261,9 @@ \textbf{sledgehammer} \postw -%Instead of issuing the \textbf{sledgehammer} command, you can also find -%Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof -%General or press the Emacs key sequence C-c C-a C-s. -%Either way, -Sledgehammer produces the following output after a few seconds: +Instead of issuing the \textbf{sledgehammer} command, you can also use the +Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output +after a few seconds: \prew \slshape @@ -345,7 +336,7 @@ Locally installed provers are faster and more reliable than those running on servers. See \S\ref{installation} for details on how to install them. -\point{Familiarize yourself with the most important options} +\point{Familiarize yourself with the main options} Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of the options are very specialized, but serious users of the tool should at least @@ -411,7 +402,7 @@ and it cannot learn. \item[\labelitemi] -An experimental, memoryful alternative to MePo is \emph{MaSh} +An experimental alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It relies on an external Python tool that applies machine learning to the problem of finding relevant facts. @@ -529,7 +520,7 @@ The \textit{metis}~(\textit{full\_types}) proof method and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed -version of Metis. It is somewhat slower than \textit{metis}, but the proof +versions of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in higher-order places (e.g., in set comprehensions). The method kicks in @@ -635,12 +626,6 @@ \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ \postw -For Proof General users, -Sledgehammer is also available in the ``Commands'' submenu of -the ``Isabelle'' menu or by pressing the Emacs key sequence C-c -C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with -no arguments in the theory text. - In the general syntax, the \qty{subcommand} may be any of the following: \begin{enum} @@ -731,16 +716,15 @@ proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. -If you use Proof General, you can instruct Sledgehammer to run automatically on -newly entered theorems by enabling the ``Auto Sledgehammer'' option in the -``Isabelle'' menu. For automatic runs, only the first prover set using +If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can +be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options +> Isabelle > 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{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict} (\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 the ``Isabelle'' menu. Sledgehammer's output is also more -concise. +and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' +option in jEdit. Sledgehammer's output is also more concise. \subsection{Metis} @@ -986,9 +970,7 @@ By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire, Yices, and Z3 in parallel---either locally or remotely, depending on the number -of processor cores available. (For historical reasons, the default value of this -option can be overridden using the option ``Sledgehammer: Provers'' in Proof -General's ``Isabelle'' menu.) +of processor cores available. It is generally a good idea to run several provers in parallel. Running E, SPASS, and Vampire for 5~seconds yields a similar success rate to running the @@ -1005,8 +987,8 @@ synchronously. The asynchronous (non-blocking) mode lets the user start proving the putative theorem manually while Sledgehammer looks for a proof, but it can also be more confusing. Irrespective of the value of this option, Sledgehammer -is always run synchronously for the new jEdit-based user interface or if -\textit{debug} (\S\ref{output-format}) is enabled. +is always run synchronously if \textit{debug} (\S\ref{output-format}) is +enabled. \optrue{slice}{dont\_slice} Specifies whether the time allocated to a prover should be sliced into several @@ -1057,10 +1039,10 @@ The traditional memoryless MePo relevance filter. \item[\labelitemi] \textbf{\textit{mash}:} -The experimental, memoryful MaSh machine learner. MaSh relies on the external -Python program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set -the environment variable \texttt{MASH} to \texttt{yes}. Persistent data is -stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}. +The experimental MaSh machine learner. MaSh relies on the external Python +program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the +environment variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in +the directory \texttt{\$ISABELLE\_HOME\_USER/mash}. \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. @@ -1090,8 +1072,8 @@ \optrue{learn}{dont\_learn} Specifies whether MaSh should be run automatically by Sledgehammer to learn the -available theories (and hence provide more accurate results). Learning only -takes place if MaSh is enabled. +available theories (and hence provide more accurate results). Learning takes +place only if MaSh is enabled. \opdefault{max\_new\_mono\_instances}{int}{smart} Specifies the maximum number of monomorphic instances to generate beyond @@ -1349,8 +1331,8 @@ \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'' in Proof General's ``Isabelle'' menu.) +For automatic runs, the ``Auto Time Limit'' option under ``Plugins > Plugin +Options > Isabelle > General'' is used instead. \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3} Specifies the maximum number of seconds that \textit{metis} or \textit{smt}