在 Coq 中导入模块

Question

我有以下文件夹结构：

- BaseDefs.v
- UsingBaseDefs.v

在这里，

BaseDefs.v

包含我想在

UsingBaseDefs.v

中使用的定义。我尝试从终端使用

coqc BaseDefs.v

命令，然后我尝试使用以下方法将模块导入

UsingBaseDefs.v

中：

Require Import BaseDefs. 

这给了我错误

找不到绑定到逻辑路径 BaseDefs 的物理路径

我在 CoqIDE 内部和另一个线程中工作（我如何在 Coq 中导入模块？）这似乎应该可行。如何解决此错误并使导入可用？

编辑：如果我使用

Print LoadPath

中的

UsingBaseDefs.v

命令打印 LoadPath，我可以看到此处未列出 BaseDefs。

Answer 1

简而言之：您可能缺少一个

_CoqProject

文件。

Coq 构建系统使用这个

_CoqProject

文件（参见 参考手册）来了解构建时哪些文件是多文件项目的一部分。因此，IDE 也使用这个系统来完成逻辑路径（在

Require Import

命令中使用的路径）和系统目录结构之间的映射。没有这样的文件，CoqIDE 不知道

BaseDefs

指的是什么。

在你的情况下，

_CoqProject

可能需要像

-R . MyProject

BaseDefs.v
UsingBaseDefs.v

与您的两个文件位于同一文件夹中。第一行告诉 Coq 将

.

文件夹映射到逻辑名称

MyProject

。接下来的两行让它知道您在该项目中拥有的两个文件。您可以在 here 找到一个更完整的 Coq 项目典型模板，例如

MakeFile

.