多文件Coq项目导入问题：编译依赖与coqtop加载方案咨询

项目结构 #

theories
  |
  *--> defn.v
  |
  *--> thm.v

无需预编译defn.v编译thm.v的方法 #

Coq的Require Import默认依赖预编译的.vo文件，但可以通过以下两种方式自动处理依赖，无需手动提前编译defn.v：

• 使用coq_makefile自动化构建
  在项目根目录创建_CoqProject文件，内容如下：

  -Q . theories
  theories/defn.v
  theories/thm.v
  

  执行以下命令生成Makefile并构建：

  coq_makefile -f _CoqProject -o Makefile
  make
  

  make会自动识别依赖顺序，先编译defn.v再编译thm.v，全程无需手动干预。
• 使用相对路径导入（Coq 8.16+）
  在thm.v中直接用相对路径导入源文件：

  Require Import "./defn.v".
  

  编译thm.v时，Coq会自动先编译defn.v并完成导入，无需提前手动编译该文件。注意这种写法依赖当前文件的相对位置，项目结构变动时需要同步调整路径。

无命令行参数在coqtop中加载defn.v的解决办法 #

你之前的报错是因为编译defn.v时的命名空间映射和coqtop中设置的不匹配：用coqc -Q . "" defn.v编译时，defn.v被归类到空命名空间（库名defn），但你在coqtop里把theories目录映射到了theories命名空间，尝试从theories导入就会出现库名不匹配的错误。

方案1：重新编译并匹配命名空间 #

1. 在theories目录的上级目录，执行编译命令：

   coqc -Q ./theories theories theories/defn.v
   

   该命令将theories目录映射到theories命名空间，编译后的defn.v对应库名theories.defn。
2. 在coqtop中执行以下命令（无需命令行参数）：

   Add LoadPath "<theories目录的绝对路径>" as theories.
   From theories Require Import defn.
   

   此时命名空间完全匹配，即可成功加载。

方案2：不重新编译，调整coqtop加载路径 #

如果不想重新编译defn.v，直接将theories目录添加到根加载路径（不映射子命名空间）：

Add LoadPath "<theories目录的绝对路径>".
Require Import defn.

这样coqtop会直接识别空命名空间下的defn库，和之前的编译结果匹配。

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