WP 生成的 Coq 文件无法编译

Question

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

当我将 Alt-ergo 与 WP 一起使用时，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 看看如何使用它。

此致，

--

文森特佩内尔。

Answer 1

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

其次，您安装软件包的顺序是相关的。特别是，如果在 frama-c 之后安装了适当版本的 coq，WP 不会编译和安装其 coq 库，而这些库正是此处所缺少的。因此，您可能需要 opam reinstall frama-c 来针对兼容的 coq 版本编译包。

WP 生成的 Coq 文件无法编译

Coq file generated by WP does not compile

coq

frama-c