linux - CoqIDE configuration in Linux

Question

I have a fresh install of Coq 8.6 in Ubuntu 17.04. When I try to compile my project using make, it works fine until I get the first error message. Then, I try to use CoqIDE to locate and correct the error, but I get new error messages, such as:

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

My guess is that something is wrong with the configuration of CoqIDE, but I do not know what that could be. Any hints?

Thanks in advance, Marcus.

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