Frama-C 23 and Coq

Question

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

Answer 1

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