Coq导入模块报错：无法找到BaseDefs逻辑路径的物理绑定

我有如下文件夹结构：

- BaseDefs.v
- UsingBaseDefs.v

其中，BaseDefs.v包含需要在UsingBaseDefs.v中使用的定义。我在终端执行了coqc BaseDefs.v命令，随后在UsingBaseDefs.v中尝试通过Require Import BaseDefs.导入模块，却收到错误：

Cannot find a physical path bound to logical path BaseDefs

我正在CoqIDE中操作，参考相关线程后仍未解决。另外，我在UsingBaseDefs.v中执行Print LoadPath命令后，发现当前目录未在加载路径列表中。请问如何解决该错误并成功导入模块？

方法1：在代码中直接添加加载路径 #

在UsingBaseDefs.v的最开头插入以下代码，将当前目录注册到Coq的加载路径：

Add LoadPath "." .
Require Import BaseDefs.

如果需要指定逻辑命名空间，也可以写成：

Add LoadPath "." as Top.
Require Import BaseDefs.

方法2：启动CoqIDE时指定加载路径 #

关闭当前CoqIDE窗口，在终端进入代码所在目录，执行以下命令启动CoqIDE：

coqide -R . Top &

-R参数会把当前目录（.）映射为逻辑命名空间Top，之后在UsingBaseDefs.v中直接使用Require Import BaseDefs.即可正常导入。

方法3：通过CoqIDE图形界面配置加载路径 #

1. 打开CoqIDE后，点击顶部菜单栏的 Coq -> Load Path...
2. 在弹出窗口中点击 Add 按钮
3. 在Directory栏选择你的代码所在文件夹，Logical Name可填写Top（或留空使用默认），按需勾选Recursive（加载子目录时需要）
4. 点击OK保存设置，重新打开UsingBaseDefs.v即可导入模块

方法4：确认编译产物存在 #

执行coqc BaseDefs.v后，检查目录下是否生成了BaseDefs.vo文件——这是Coq的编译产物，没有该文件的话，即使加载路径正确也无法导入。如果未生成，排查BaseDefs.v的语法错误后重新编译。

内容的提问来源于stack exchange，提问作者Tilman Zuckmantel