WP 生成的 Coq 文件无法编译答案

【问题标题】：Coq file generated by WP does not compileWP 生成的 Coq 文件无法编译
【发布时间】：2019-03-08 15:32:05
【问题描述】：

我已经通过 opam 安装了 frama-c (18.0) 和 coqide (8.9)（当然还有其他需要的依赖项，但这可能不是这里的问题）。关键是我只是通过 opam 安装它，没有做任何其他奇怪的事情（而且我没有看到任何我应该做的特定指令）。

当我在 WP 中使用 Alt-ergo 时，Frama-c 按预期工作，但如果我尝试使用 coq 或 coqide 而不是 Alt-ergo，那么对于 Qed 无法立即证明的每个目标，我都会收到以下错误：

[wp] 13 goals scheduled
[wp] [Coq] 'Qed.v' compilation failed.
------------------------------------------------------------
--- Coqc (stderr) :
------------------------------------------------------------
File "/tmp/wp7fe5dc.dir/coqwp/Qed.v", line 27, characters 8-17:
Error:
Cannot find a physical path bound to logical path matching suffix bool.

------------------------------------------------------------
[wp] [Coq] Goal typed_nondet_loop_inv_preserved : Failed
  Compilation of 'Qed.v' failed.

请注意，在显示错误之前，它会编译一些其他 .v 文件。我试图手动打开 coqide 中的文件，我得到了相同的结果。作为记录，这里是 coq 抱怨的几行：

Require bool.Bool.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.

我也尝试将 coq 降级一点，但不低于 8.7（否则 opam 会抱怨基本安装包不兼容，我真的不想搞砸我的安装），并得到了相同的结果。

如果有人知道造成这种情况的原因以及我如何正确设置它，那就太好了。即使对于我现在用它做的事情，Alt-ergo 就足够了，我还是想玩一下 coq 看看它是如何使用的。

问候，

文森特·佩内尔。

【问题讨论】：

标签： coq frama-c

【解决方案1】：

首先，如果您想将它与 Frama-C/WP 一起使用，确实需要 coq 8.8（例如 8.7.2），因为目前不支持较新的版本。

其次，您安装软件包的顺序是相关的。特别是，如果在frama-c 之后安装了适当版本的coq，则WP 没有编译和安装它的coq 库，这是这里缺少的。因此，您可能需要使用opam reinstall frama-c 来针对兼容的coq 版本编译包。

【讨论】：

您好，非常感谢您的回答。确实是这样。顺便问一下这个愚蠢的问题，我以为我已经尝试过了，看来我之后忘记重新编译 frama-c 了。问候，
很高兴能帮上忙。你的问题并不愚蠢（我赞成?）：在这种情况下，WP 至少可以提供更有用的错误消息（例如关于缺少 Coq 库的警告），并且frama-c 的opam 包可以改进有点它的可选依赖项。