Search code examples
coq

Compiling multiple Coq files does not work

I'm really lost on how to actually use multiple files in Coq. I was trying to follow these directions.

I have two files.

src/a.v:

Definition bar: nat := 1.

src/b.v:

Require Import a.

Definition foo := bar.

I attempt to compile as such:

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

I get the following error:

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

I can't find any clear information on how you actually compile with multiple files

Solution

  • I recommend you perform two calls to coqc, first with a then with b. Having multiple files in the argument command line is actually not supported [we will improve the interface in next versions as to warn about this]