我在Ubuntu 17.04中全新安装了Coq 8.6.当我尝试使用make编译我的项目时,它工作正常,直到我收到第一条错误消息.然后,我尝试使用CoqIDE来定位并更正错误,但是我收到了新的错误消息,例如:
"文件foo.vo包含库Top.foo而不是库foo"
我的猜测是CoqIDE的配置出了问题,但我不知道那可能是什么.任何提示?
提前谢谢,马库斯.
我猜你现在站在文件目录中 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)