1

After installing Frama-C (23), Why3, and Coq on macOS I ran the command

rm -f ~/.why3.conf ; why3 config detect

The following message was shown

Found prover Coq version 8.10.2, but no Why3 libraries were compiled for it
  • Does this mean I cannot use coq with Frama-C?
  • How do I instruct opam to compile the above mentioned Why3 libraries?

Regards

Night Heron
  • 11
  • 1

1 Answers1

0

I would say that it might be more a Why3 question than a Frama-C question. Anyway, you have to install the Opam package why3-coq so that you have Why3 libraries compiled for Coq (and then re-execute why3 config detect).

Ksass'Peuk
  • 538
  • 2
  • 12