WP生成的Coq文件无法编译

问题描述 投票:2回答:1

我已经通过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。

coq frama-c
1个回答
1
投票

首先,如果你想将它与Frama-C / WP一起使用,你确实需要coq <8.8(例如8.7.2),因为目前不支持更新的版本。

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

© www.soinside.com 2019 - 2024. All rights reserved.