From 23dc0c272249554e372596e9e617b29ee731e970 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 13 Sep 2019 10:57:50 +0200
Subject: [PATCH] [opam] fix for wp
- deprecation messages for alt[gr]-ergo and coq[ide]
- require why3 >= 1.2.0 (includes conflicts with why3-base)
- no more need for why3-coq
---
opam/opam | 17 +++++------------
1 file changed, 5 insertions(+), 12 deletions(-)
diff --git a/opam/opam b/opam/opam
index 83422183701..05aa26d252a 100644
--- a/opam/opam
+++ b/opam/opam
@@ -97,7 +97,7 @@ depends: [
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
"yojson"
- "why3"
+ "why3" { >= "1.2.0" }
]
depopts: [
@@ -105,14 +105,11 @@ depopts: [
# Coq: because .vo would would not be loadable by another version of Coq
# libraries: because we use dynamic linking
"coq"
- "why3-coq"
"mlgmpidl"
"apron"
]
conflicts: [
- "why3-base" #for WP plug-in
- "why3" { < "1.2.0" } #for WP plug-in
"lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1
"frama-c-e-acsl" #avoid mixing old releases of E-ACSL, it is already
#distributed with this version of Frama-C
@@ -121,12 +118,8 @@ conflicts: [
]
messages: [
- "Coq can be used with the WP plug-in for proving interactively proof obligations"
- {!coq:installed}
- "Alt-Ergo Graphical Interface can be used by the WP plug-in"
- {!altgr-ergo:installed & alt-ergo <= "1.30"}
- "Note: the package altgr-ergo could prevent the installation of newer versions of Alt-Ergo"
- {!altgr-ergo:installed & alt-ergo <= "1.30" & ocaml >= "4.04.0"}
- "Note: the installed package altgr-ergo could prevent the installation of newer versions of Alt-Ergo"
- {altgr-ergo:installed & ocaml >= "4.04.0"}
+ "The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
+ {alt-ergo:installed}
+ "The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
+ {coq:installed}
]
--
GitLab