Linux中的CoqIDE配置

Mar*_*cus 2 linux coq coqide

我在Ubuntu 17.04中全新安装了Coq 8.6.当我尝试使用make编译我的项目时,它工作正常,直到我收到第一条错误消息.然后,我尝试使用CoqIDE来定位并更正错误,但是我收到了新的错误消息,例如:

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

我的猜测是CoqIDE的配置出了问题,但我不知道那可能是什么.任何提示?

提前谢谢,马库斯.

lar*_*rsr 5

我猜你现在站在文件目录中 foo.vo

要将当前目录中的文件映射.到命名空间,Top请提供参数

-Q . Top
Run Code Online (Sandbox Code Playgroud)

这是一个"完整"的例子.

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
Run Code Online (Sandbox Code Playgroud)

但是使用coqtop而不将.vo映射到编译它的命名空间失败:

coqtop

Coq <  Require foo.

> Require foo.
> ^^^^^^^^^^^^
Error: The file /.../test/foo.vo contains library Top.foo
and not library foo
Run Code Online (Sandbox Code Playgroud)