linux - Linux 中的 CoqIDE 配置

Question

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

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

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

提前致谢，马库斯。

Answer 1

我猜你现在正站在文件 foo.vo

的目录中

要将当前目录 . 中的文件映射到命名空间 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

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

coqtop

Coq <  Require foo.

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