Linux中的CoqIDE配置

Question

我有一个新的安装Coq 8.6在Ubuntu17.04。当我试图使用make编译我的项目时，它可以正常工作，直到我得到第一条错误消息。然后，我尝试使用CoqIDE来定位和更正错误，但是我得到了新的错误消息，例如：

“文件foo.vo包含库Top.foo而不是库foo”

我的猜测是CoqIDE的配置有问题，但我不知道这可能是什么。有什么暗示吗？

提前谢谢马库斯。

Answer 1

我想您现在站在目录中的文件是foo.vo

若要将当前dir .中的文件映射到命名空间Top中，请给出参数

-Q . Top

这里是一个“完整”的例子。

mkdir test; cd test
echo 'Definition a:=1.' > foo.v

coqc -Q . Top foo.v    # this puts the foo module into Top as Top.foo.

coqtop -Q . Top

Coq <  Require Import Top.foo. Print a.

a = 1
     : nat

但是，在不将.vo映射到编译它的名称空间的情况下使用coqtop失败：

coqtop

Coq <  Require foo.

> Require foo.
> ^^^^^^^^^^^^
Error: The file /.../test/foo.vo contains library Top.foo
and not library foo