Build Why3 with Coq support

[suhr]

Right now creusot-install builds Why3 without Coq support, even if Coq is installed in the system.

[Lysxia]

You can install Coq in Creusot's switch and it will stay there:

opam install --switch ~/.local/share/creusot coq

That said our current stance is to encourage making proofs automatable with why3find. I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

[suhr]

Why3 documentation says that Coq must be installed before building Why3:

If you want to use the Coq realizations (Section 10.2), then Coq has to be installed before Why3. Look at the summary printed at the end of the configuration script to check if Coq has been detected properly. Similarly, in order to use PVS (Section 10.5) or Isabelle (Section 10.4) to discharge proofs, PVS and Isabelle must be installed before Why3. You should check that those proof assistants are correctly detected by the configure script.

(https://www.why3.org/doc/install.html)

I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

To investigate why a particular invariant does not work. In Why3, the only way to debug an invariant is to read a rather unreadable goal. While in a proof assistant, I could simplify the goal and try to prove it yourself to figure out why it's not provable.

[Lysxia]

That's a quote from the instructions for installing from source. On opam you can install why3-coq independently.

(I previously thought installing Coq would rebuild Why3 for Coq support, but instead installing why3-coq seems to be the way to go.)

[suhr]

I see, thanks. Though opam install --switch ~/.local/share/creusot why3-coq does not work, because it requires why3 <= 1.8.0.

[Lysxia]

Run opam update to refresh opam's package database. nevermind

[Lysxia]

Now that I think about it, you may want manage the installation of Why3 and Coq manually with a global opam switch instead, because it will make it less of a hassle to work with Coq (notably for editor extensions to find it):

opam install why3 why3find why3-ide why3-coq
./INSTALL --external why3-and-why3find

[suhr]

I guess I need to patch creusot-deps.opam, so it does not use git versions of packages for which there's no why3-coq version.

[claudemarche]

I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

To investigate why a particular invariant does not work. In Why3, the only way to debug an invariant is to read a rather unreadable goal. While in a proof assistant, I could simplify the goal and try to prove it yourself to figure out why it's not provable.

Notice that in Why3 IDE, you can also manually apply some transformations and simplifications to do what what you want, that is to figure out why an invariant is not provable.

That being said, I would certainly agree that when you have the knowledge of a proof assistant, like Coq, you would prefer to do that with that particular assistant.

And a final remark: it is true that Why3 currently does not offer Lean as a back-end, but we would certainly be happy to accept patches to make it work!