From 025a391898acfe24d5e0d8b64dbb1faa0ab40ecf Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 30 Oct 2020 10:44:02 +0100
Subject: [PATCH] [wp] Fixes Coq compilation constraints
---
opam/opam | 2 +-
src/plugins/wp/configure.ac | 6 ++----
2 files changed, 3 insertions(+), 5 deletions(-)
diff --git a/opam/opam b/opam/opam
index f60fee39900..2f5ce948ce2 100644
--- a/opam/opam
+++ b/opam/opam
@@ -132,6 +132,6 @@ depopts: [
messages: [
"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)."
+ "The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.12.x (use TIP or Why-3 instead)."
{coq:installed}
]
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 052fd1617d8..fd5332ac585 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -85,16 +85,14 @@ if test "$ENABLE_WP" != "no"; then
if test "$COQC" = "yes" ; then
COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
- 8.7*|8.8*|8.9*|8.10*|8.11.*|8.12.*|trunk)
+ 8.12.*|trunk)
AC_MSG_RESULT(coqc version $COQVERSION found)
;;
*)
- AC_MSG_RESULT(unsupported coqc version $COQVERSION)
+ AC_MSG_RESULT(unsupported coqc version $COQVERSION for - deprecated - native backend)
COQC="no"
;;
esac
- else
- AC_MSG_NOTICE(rerun configure to make wp using coq 8.7.2 or higher)
fi
else
COQC="no"
--
GitLab