Frama-C 23和Coq

Question

在macOS上安装Frama (23)、Why3和Coq之后，我运行以下命令

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

显示了以下消息

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

• ，这是否意味着我不能在Frama-C？
• 中使用coq ?如何指示opam编译上述Why3库？

问候

Answer 1

我想说，与其说这是一个Frama问题，不如说是一个Why3问题。无论如何，您必须安装Opam包why3-coq，以便为Coq编译Why3库(然后重新执行why3 config detect)。