编译多个 Coq 文件不起作用

Question

我真的不知道如何在 Coq 中实际使用多个文件。我试图关注these directions。

我有两个文件。

src/a.v:

Definition bar: nat := 1.

src/b.v:

Require Import a.

Definition foo := bar.

我尝试这样编译：

coqc -R src "" src/a.v src/b.v

我收到以下错误：

user@machine:~/code/coq$ coqc -R src "" src/a.v src/b.v
While loading initial state:
Loading file /home/user/code/coq/src/.b.aux: aux file name mismatch

我找不到任何关于您如何实际编译多个文件的明确信息

Answer 1

我建议您对coqc 执行两次调用，首先调用a，然后调用b。实际上不支持在参数命令行中包含多个文件[我们将在下一个版本中改进界面以警告这一点]