我已经通过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,看看它是如何使用的。
问候,
--
Vincent Penelle。
首先,如果你想将它与Frama-C / WP一起使用,你确实需要coq
<8.8
(例如8.7.2
),因为目前不支持更新的版本。
其次,您安装软件包的顺序是相关的。特别是,如果在coq
之后安装了适当版本的frama-c
,WP
没有编译和安装它的coq库,这些库是这里缺少的。因此,您可能希望使用opam reinstall frama-c
来编译兼容的coq
版本的软件包。