When I go to C:\GNAT\2020\libexec\spark\bin and run ".\why3-config --detect-provers" I get such answer about Coq:

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

Does anyone know how to compile necessary libraries so that they can be used during manual proof with Coq?

hmm, I don't think Coq 8.5 is supported. I believe you need both the opam packages `why3`

and `why3-coq`

. When both are installed with a modern version of Coq, I can replay the following mixed Alt-Ergo and Coq proof: https://github.com/coq-community/bertrand/tree/master/why

it should be noted that why3 and its Coq library are separate from GNAT or Frama-C, etc. So if the basic Why3 Coq machinery is not working, then it definitely will not work through some UI...

From https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/alternative_provers.html:

gnatprove has support for the Coq interactive prover, even though Coq is not part of the SPARK distribution. If you want to use Coq with SPARK, you need to install it yourself on your system and put it in your PATH environment variable. Then, you can simply provide --prover=coq to gnatprove. Note that the only supported version currently is Coq 8.5.

I'm trying to run it through GNAT studio using included why3. I haven't installed anything using OPAM.

if they are using a Why toolchain tied to Coq 8.5, then basically you are tied to a dinosaur full of bugs

I can confirm that Why 1.3.3 works quite well with Coq (8.12.0) in general, but anything before that has been very hit and miss, even at the time they were released

Windows is unfortunately likely to make everything twice as hard if you really want a toolchain based on 8.5 to work...

@Lessness without clicking links, it seems you’re mentioning GNAT *2020* but linking to *SPARK2014*. Is there any hope they’ve upgraded the supported Coq version?

sorry, nevermind, stupid question.

Last updated: Dec 07 2023 at 18:01 UTC