macos - Frama-C 23 和 Coq

Question

在 macOS 上安装 Frama-C (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

• 这是否意味着我不能将 coq 与 Frama-C 一起使用？
• 如何指示 opam 编译上述Why3 库？

问候

Answer 1

我会说这可能更像是一个 Why3 问题而不是 Frama-C 问题。无论如何，您必须安装 Opam 包why3-coq，以便为 Coq 编译 Why3 库（然后重新执行why3 config detect）。