Stream: Miscellaneous

Topic: Using Coq in GNAT Studio

view this post on Zulip Lessness (Nov 03 2020 at 13:19):

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?

view this post on Zulip Karl Palmskog (Nov 03 2020 at 13:22):

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

view this post on Zulip Karl Palmskog (Nov 03 2020 at 13:24):

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...

view this post on Zulip Lessness (Nov 03 2020 at 13:39):

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.

view this post on Zulip Lessness (Nov 03 2020 at 13:40):

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

view this post on Zulip Karl Palmskog (Nov 03 2020 at 13:40):

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

view this post on Zulip Karl Palmskog (Nov 03 2020 at 13:42):

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

view this post on Zulip Karl Palmskog (Nov 03 2020 at 13:45):

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

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 14:08):

@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?

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 14:10):

sorry, nevermind, stupid question.

Last updated: Dec 07 2023 at 18:01 UTC