author blanchet Wed, 21 May 2014 14:09:43 +0200 changeset 57040 fc96f394c7e5 parent 57039 1ddd1f75fb40 child 57041 aceaca232177 child 57042 5576d22abf3c
docs
--- a/src/Doc/Nitpick/document/root.tex	Wed May 21 14:09:43 2014 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Wed May 21 14:09:43 2014 +0200
@@ -143,33 +143,33 @@
\section{Installation}
\label{installation}

-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).
-
-There are two main ways of installing Kodkodi:
-
-\begin{enum}
-\item[\labelitemi] If you installed an official Isabelle package,
-it should already include a properly setup version of Kodkodi.
-
-\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
-from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
-line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% -\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
-startup. Its value can be retrieved by executing \texttt{isabelle}
-\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to Kodkodi. For example, if the
-\texttt{components} file does not exist yet and you extracted Kodkodi to
-\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
-
-\prew
-\texttt{/usr/local/kodkodi-1.5.2}
-\postw
-
-(including an invisible newline character) in it.
-\end{enum}
+Nitpick is part of Isabelle, so you do not need to install it. It relies on a
+third-party Kodkod front-end called Kodkodi, which in turn requires a Java
+virtual machine. Both are provided as official Isabelle components.
+
+%There are two main ways of installing Kodkodi:
+%
+%\begin{enum}
+%\item[\labelitemi] If you installed an official Isabelle package,
+%it should already include a properly setup version of Kodkodi.
+%
+%\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
+%from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
+%line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% +%\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
+%startup. Its value can be retrieved by executing \texttt{isabelle}
+%\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
+%file with the absolute path to Kodkodi. For example, if the
+%\texttt{components} file does not exist yet and you extracted Kodkodi to
+%\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
+%
+%\prew
+%\texttt{/usr/local/kodkodi-1.5.2}
+%\postw
+%
+%(including an invisible newline character) in it.
+%\end{enum}

To check whether Kodkodi is successfully installed, you can try out the example
in \S\ref{propositional-logic}.
--- a/src/Doc/Sledgehammer/document/root.tex	Wed May 21 14:09:43 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed May 21 14:09:43 2014 +0200
@@ -14,6 +14,9 @@

+\let\oldS=\S
+\def\S{\oldS\,}
+
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}

@@ -601,8 +604,8 @@
Problems can be easy for \textit{auto} and difficult for automatic provers, but
the reverse is also true, so do not be discouraged if your first attempts fail.
Because the system refers to all theorems known to Isabelle, it is particularly
-suitable when your goal has a short proof from lemmas that you do not know
+suitable when your goal has a short proof but requires lemmas that you do not

\point{Why are there so many options?}

@@ -614,6 +617,7 @@
\label{command-syntax}

\subsection{Sledgehammer}
+\label{sledgehammer}

Sledgehammer can be invoked at any point when there is an open goal by entering
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
@@ -728,6 +732,7 @@
also more concise.

\subsection{Metis}
+\label{metis}

The \textit{metis} proof method has the syntax

@@ -1087,7 +1092,9 @@
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the Mash'' option under Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit. Persistent data for both engines is stored in the directory -\texttt{\$ISABELLE\_HOME\_USER/mash}.
+\texttt{\$ISABELLE\_HOME\_USER/mash}. When switching to the \textit{py} engine, +it is recommended to invoke the \textit{relearn\_isar} subcommand +(\S\ref{sledgehammer}) to synchronize the Python persistent databases. \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. @@ -1102,10 +1109,10 @@ takes a value that was empirically found to be appropriate for the prover. Typical values range between 50 and 1000. -For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover}, -\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the -maximum number of facts from the background library that should be learned -($\infty$by default). +For the MaSh-related subcommands \textit{learn\_isar}, \textit{learn\_prover}, +\textit{relearn\_isar}, and \textit{relearn\_prover} (\S\ref{sledgehammer}), +this option specifies the maximum number of facts from the background library +that should be learned ($\infty\$ by default).

\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
Specifies the thresholds above which facts are considered relevant by the
@@ -1216,7 +1223,7 @@
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
Like for \textit{poly\_guards} constants are annotated with their types to
\textbf{%