From a3cea6c46ecb2682409e451460ceb7289daab09e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 2 Oct 2020 11:20:33 +0200
Subject: [PATCH] [wp/doc] Update interactive mode options
---
src/plugins/wp/doc/manual/wp_plugin.tex | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index a690b944e0e..39ba32bc5e3 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -995,12 +995,16 @@ See \texttt{-wp-interactive <mode>} option for details.
For each goal, the first decision procedure that succeeds cancels the
other attempts.
\item[\tt -wp-interactive <mode>] selects the interaction mode with
- interactive provers such as Coq. Three modes are available:
- \texttt{"batch"} mode only check existing scripts (the default);
- \texttt{"edit"} mode opens the default prover editor on each generated goal;
- \texttt{"fix"} mode only opens
- editor for non-proved goals. New scripts are created in the \texttt{interactive}
- directory of \textsf{WP} session (see option \texttt{-wp-session <dir>}).
+ interactive provers such as Coq. Five modes are available:
+ \begin{itemize}
+ \item \texttt{"batch"} mode only check existing scripts (the default);
+ \item \texttt{"update"} mode update the script and then checks it;
+ \item \texttt{"edit"} mode opens the default prover editor on each generated goal;
+ \item \texttt{"fix"} mode only opens editor for non-proved goals;
+ \item \texttt{"fixup"} combines \texttt{"update"} and \texttt{"fix"} (if necessary).
+ \end{itemize}
+ New scripts are created in the \texttt{interactive} directory of \textsf{WP}
+ session (see option \texttt{-wp-session <dir>}).
\item[\tt -wp-detect] lists the provers available for \textsf{Why-3}.
This command can only work if \textsf{why3} API was installed before building and
installing \textsf{Frama-C}.
--
GitLab