Frama-C/WP and Why3

[jensgerlach]

Again, all remarks refer to xubuntu-18.04.

It looks like as if Frama-C/WP implicitly assumes that why3 is not newer than 0.88.3 and that coq is not newer 8.7.2. If this is the case , then the installation of Frama-C should not allow the installation of newer, unsupported why3 versions.

---

The reason I assume this comes from the following observation. If I don't pin why3 to 0.88.3 and thus install the most reason versions of why3 (1.1.0) and `coqide (8.8.2), then I receive later the warning

Found prover Coq version 8.8.2, but no Why3 libraries were compiled for it

[correnson]

Thanks for the feedback Jens. The configuration phase for Frama-C is supposed to check why3 and coq versions. With versions different from 0.88. (for why3) and 8.7. (for coq) the Frama-C configure shall complain. Is this not the case in your situation ?

[hyarion]

The same thing happens on macos (mojave, 10.14.1) when following the guide from https://frama-c.com/install-18.0-Argon.html#installing-frama-c-on-macos using opam from a (more or less) clean install

You end up with ocaml.4.07.1, frama-c.18.0, why3.1.1.0, coq.8.8.2, alt-ergo.2.2.0 without anything complaining during the installation. (log can be attached if needed)

If you run why config --detect-provers afterwards, it reports:

$ why3 config --detect-provers
Found prover Alt-Ergo version 2.2.0, OK.
Found prover Coq version 8.8.2, but no Why3 libraries were compiled for it
1 prover(s) added
Generating strategies:
  Prover Alt-Ergo 2.2.0 will be used in Auto level >= 1
Save config to /Users/<username>/.why3.conf
...

[hyarion]

It seems like why3 went through a change for the 1.0.0 version. Before that version they had two packages, why3 and why3-base, but when 1.0.0 was introduced they seem to have deprecated the why3-base package as it never got a new version. My guess is that whatever was in why3-base is now located in why3 for 1.0.0+

When looking at the opam definition file for frama-c I notice that it never changed from why3-base to why3 in the conflict section. https://github.com/Frama-C/Frama-C-snapshot/blob/2f7a0eee0a8083374236da6a59a8d500de00305d/opam/opam#L107

The following change make the frama-c complain as @correnson mention it should.

--- "why3-base" { < "0.88" | >= "1.0.0" } #for WP plug-in
+++ "why3-base" { < "0.88"} #for WP plug-in
+++ "why3" { >= "1.0.0" } #for WP plug-in

[maroneze]

Thank you @hyaron, we fixed the opam package to use the why3 constraints as you suggested.

[hyarion]

The reason I assume this comes from the following observation. If I don't pin why3 to 0.88.3 and thus install the most reason versions of why3 (1.1.0) and coqide (8.8.2), then I receive later the warning

Found prover Coq version 8.8.2, but no Why3 libraries were compiled for it

Just for reference, this error message is what you get if you install >= why3 1.0.0 and coq but don't install why3-coq.

[jensgerlach]

Why not automatically install why3-coq if coq and why3 are requested by the user. (I have just run into this problem while experimenting with Frama-C 19.0 (beta2))

[bobot]

I don't know how to do that with opam.

[yakobowski]

I think the "standard" solution is to have why3-coq inside the why3 package, and Opam will recompile why3 when Coq is installed. But I imagine there are good reasons to have 2 packages for why3/why3-coq.

[bobot]

Yes people can ask why3-coq and have automatically why3 and coq, and if coq change why3 doesn't have to be recompiled.

But we can add a message (printed at the end of installation) in the why3 package that the package why3-coq exists.

[jensgerlach]

I think this issue can be closed now.