frama-c - 在cygwin中安装frama-c时出错

Question

我正在尝试在 cygwin 中安装 frama-c 并收到以下错误，但我无法解释它们。你能帮我解释一下，或者给我一个链接到我从哪里得到信息吗？

Preparing    Wp-Coq Sources
Uncaught exception: Util.UserError("_", _)
Makefile:49: recipe for target `depend' failed
make[1]: *** [depend] Error 2
src/wp/Makefile:285: recipe for target `.make-wpcoqs' failed
make: *** [.make-wpcoqs] Error 2

请注意，coqc 和 ocaml 都是最新版本

Answer 1

您是否有机会使用 Coq 8.4？我遇到了非常相似的事情，我的问题是-coqlib <your Coq installation directory>当 Coq 未安装在 PATH 的标准目录中时缺少该选项。Coq 8.3 中曾经有一个特定的错误消息，但它似乎在 Coq 8.4 中消失了。

如果您可以在 Makefile 中找到运行该coqdep命令的行，并将其替换为类似的内容coqdep -coqlib ~/coq84pl1（替换~/coq84pl1为您的 Coq 安装目录），它就可以工作。但是您还需要将此标志添加到其他与 Coq 相关的命令中（coqc例如），否则可能稍后会出现其他问题。