From 3b9620db6fba86b0142db01bf72394022e1ee466 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 17 Sep 2019 12:29:39 +0200
Subject: [PATCH] [wp/doc] update changelog & manual
---
src/plugins/wp/Changelog | 12 ++++++++----
src/plugins/wp/doc/manual/wp_plugin.tex | 4 ++--
2 files changed, 10 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 46d91b13189..83554c51729 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,11 +20,15 @@
# <Prover>: prover
###############################################################################
-- WP [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
+- TIP [2019/09/17] Using all selected Why-3 provers for proof search
+- Gui [2019/09/17] Updated panel for provers, models, cache, etc.
+- WP [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
+-! WP [2019/09/17] Deprecated native alt-ergo & coq output, see -wp-prover option
+-! WP [2019/07/05] -wp-prover <p> now defaults to <why3:p> (including default alt-ergo)
+-! WP [2019/07/05] Use native Why3 API (now requires why3 at compile time)
- WP [2019/06/27] Improving Cint simplifier and quantifier introduction
-o WP [2019/06/27] Using the new API of Qed
-o Qed [2019/06/27] Changes into the API in order to get a more secure way to manipulate quantifiers and binding
-- Qed [2019/05/09] Transforms some boolean quantifications into let constructs
+o Qed [2019/06/27] More secure API for quantifier management
+- Qed [2019/05/09] Transform (some) boolean quantifications into variable assignments
##########################
Plugin WP 19.0 (Potassium)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 1adc2340ce9..d582a2d2640 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1380,8 +1380,8 @@ The cache can only be used with \textsf{Why-3} provers, it does not work with na
The main option to control cache usage is \verb+-wp-cache+, documented below:
\begin{description}
-\item[\tt -wp-cache <mode>] selects the cache mode to use with why3 provers. The default mode is \verb'update' if \verb+-wp-session+ is set, and \verb+none+ otherwize. The cache entries
-are stored in the session directory, which would be \verb+./frama-c/wp/cache+ by default.
+\item[\tt -wp-cache <mode>] selects the cache mode to use with why3 provers. The default mode is \verb'update' if \verb+-wp-session+ is set or when using the Frama-C/Gui, and \verb+none+ otherwize. The cache entries
+are stored in the session directory, which is \verb+./frama-c/wp/cache+ by default.
\end{description}
The available cache modes are described below:
--
GitLab