diff --git a/reference-configuration.md b/reference-configuration.md index 67657200acdd65fd4798d090e3865c5e88fb7d3d..bd5f5d3d5ba6bd052d840d22830712029d6edc00 100644 --- a/reference-configuration.md +++ b/reference-configuration.md @@ -2,14 +2,14 @@ The following set of packages is known to be a working configuration for compiling Frama-C+dev, on a machine with gcc <= 9[^gcc-10] - OCaml 4.08.1 -- alt-ergo.2.0.0 (for wp, optional) +- alt-ergo.2.3.3 (for wp, optional) - apron.v0.9.12 (for eva, optional) - lablgtk.2.18.11 | lablgtk3.3.1.1 + lablgtk3-sourceview3.3.1.1 - mlgmpidl.1.2.12 (for eva, optional) - ocamlfind.1.8.1 - ocamlgraph.1.8.8 - ppx_deriving_yojson.3.5.2 (for mdr, optional) -- why3.1.3.1 +- why3.1.3.3 - yojson.1.7.0 - zarith.1.9.1 - zmq.5.1.3 (for server, optional) diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac index 0c3828b35ff2f37b6daf675d0e6670ce9639c3fc..052fd1617d8adadc08240f26a10416921815c5c1 100644 --- a/src/plugins/wp/configure.ac +++ b/src/plugins/wp/configure.ac @@ -63,15 +63,15 @@ case $WHY3VERSION in AC_MSG_RESULT([not found!]) plugin_disable(wp,[why3 not found]) ;; - 0.* | 1.[[012]].* | 1.3.0) - AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.1+]) + 0.* | 1.[[012]].* | 1.3.0 | 1.3.1 | 1.3.2) + AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.3+]) plugin_disable(wp,[non-supported why3 $WHY3VERSION]) ;; 1.3.*) AC_MSG_RESULT([found $WHY3VERSION: ok]) ;; *) - AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.1+)]) + AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.3+)]) ;; esac fi @@ -85,7 +85,7 @@ 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.*|trunk) + 8.7*|8.8*|8.9*|8.10*|8.11.*|8.12.*|trunk) AC_MSG_RESULT(coqc version $COQVERSION found) ;; *)