coq - 为什么在 coqide 中使用 _CoqProject 的 `make` 与命令行上的 `coqc` 不同？

Question

我有两个短文件:cc_test 由引理 cc: 4 = 4. 证明。汽车。 Qed.libtest 由需要导入 cc_test。检查抄送。

当我执行coqc -R 。 ClosureLib -top ClosureLib cc_test在目录“/home/barry/svn/Coq/Closure_Calculus”和coqc -R "/home/barry/svn/Coq/Closure_Calculus"ClosureLib libtest在它的目录中，我得到了预期的输出cc: 4 = 4

但是，当上述 coqc 的参数(从 -R 到末尾)放在 _CoqProject 文件中时，我调用 Make makefile 然后从 coqide 调用 Make菜单，cc_test 没问题，但 libtest 产生输出文件“./libtest.v”，第 1 行，字符 15-22:
错误:无法找到库 cc_test。

我应该如何修改项目文件才能使其正常工作？

评论:coq 引用手册(第 15 章)没有提及这些方法之间的任何区别。此外，参数“-top ClosureLib”在命令行方法中似乎是必要的，但使用 make 似乎无关紧要，因为在其他实验中，我经常收到错误消息，说它找到了 Top.foo 而不是 ClosureLib.foo。

Answer 1

首先，我不认为 -top ClosureLib 在这里有用。 documentation将 -top 描述为

Not valid for coqc as the toplevel module name is inferred from the name of the output file

至于你的主要问题，我必须承认我的解决方案是使用安装依赖项

coq_makefile -f _CoqProject -o Makefile
make
make install

make install 将库放在 user-contrib 中，它们将自动加载的地方。然后，您可以直接使用 Require。

编辑:

感谢@Zimm48，我了解了如何使用 $COQPATH 完成相同的任务，而无需先安装依赖项。但是文件夹的名称将用作逻辑前缀，因此您必须在 -R 或 -Q 参数中使用与目录名称相同的标识符.

我建议使用以下架构:

• 在目录 /home/barry/svn/Coq/ClosureLib 中(请注意，我重命名了目录，因此它的名称与传递给 -R< 的标识符相同), _CoqProject 包含

  -R . ClosureLib
  cc_test.v
  

  你编译 cc_test.v 如下:

  coq_makefile -f _CoqProject -o Makefile
  make
  

• 在包含libtest.v的目录中，_CoqProject包含

  -R . MyLib
  libtest.v
  

  您可以按如下方式编译libtest.v:

  coq_makefile -f _CoqProject -o Makefile
  COQPATH=/home/barry/svn/Coq make