Skip to content
Snippets Groups Projects
Commit 1c1b355b authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'fix/wp/coq-version-constraints' into 'stable/titanium'

Fixes Wp-Coq version constraints

See merge request frama-c/frama-c!2924
parents f9610df7 025a3918
No related branches found
No related tags found
No related merge requests found
...@@ -132,7 +132,7 @@ depopts: [ ...@@ -132,7 +132,7 @@ depopts: [
messages: [ messages: [
"The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)" "The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
{alt-ergo:installed} {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} {coq:installed}
] ]
......
...@@ -85,16 +85,14 @@ if test "$ENABLE_WP" != "no"; then ...@@ -85,16 +85,14 @@ if test "$ENABLE_WP" != "no"; then
if test "$COQC" = "yes" ; then if test "$COQC" = "yes" ; then
COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' ` COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in 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(coqc version $COQVERSION found)
;; ;;
*) *)
AC_MSG_RESULT(unsupported coqc version $COQVERSION) AC_MSG_RESULT(unsupported coqc version $COQVERSION for - deprecated - native backend)
COQC="no" COQC="no"
;; ;;
esac esac
else
AC_MSG_NOTICE(rerun configure to make wp using coq 8.7.2 or higher)
fi fi
else else
COQC="no" COQC="no"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment