Linux 中的 CoqIDE 配置

Question

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

"The file foo.vo contains library Top.foo and not library foo"

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

提前致谢，马库斯.

Answer 1

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

所在的目录中

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

-Q . Top

这是一个 "complete" 示例。

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

Linux 中的 CoqIDE 配置

CoqIDE configuration in Linux

linux

coq

coqide