3

我有两个短文件： cc_test Lemma cc: 4 = 4. Proof. auto. Qed. 和 libtest 给出 Require Import cc_test. Check cc.

当我 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 文件中，然后我从 coqide 菜单中调用Make makefile，Makecc_test 没问题，但 libtest 产生输出 File "./libtest.v", line 1, characters 15-22: Error: Unable to locate library cc_test.

我应该如何修改项目文件以使其工作？

评论：coq 参考手册（第 15 章）没有提到这些方法之间的任何区别。此外，参数“-top ClosureLib”在命令行方法中似乎是必需的，但似乎并不重要，make因为在其他实验中，我经常收到错误消息，说它找到了 Top.foo 但没有找到 ClosureLib.foo。

4

1 回答 1

2

首先，我认为-top ClosureLib这里没有用。该文档描述-top为

对 coqc 无效，因为顶层模块名称是从输出文件的名称推断出来的

至于您的主要问题，我必须承认我的解决方案是使用

coq_makefile -f _CoqProject -o Makefile
make
make install

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

编辑：

感谢@Zimm48，我了解了如何使用$COQPATH来完成相同的任务，而无需先安装依赖项。但是文件夹的名称将用作逻辑前缀，因此您必须在-Ror-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
于 2017-11-07T14:15:49.213 回答