The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I deleted a .v file and forgot to remove it from `_CoqProject`. Suddenly, I was getting too many errors that indicated that `make` is trying to compile files in an order that disrespects the dependencies.

Here is a minimal example to illustrate the problem:

[abhishek@optiplex temp]$ ls
A.v  B.v  _CoqProject

[abhishek@optiplex temp]$ cat B.v  
Require Import Test.A.

Definition y :=4.

[abhishek@optiplex temp]$ cat _CoqProject  
-Q . Test

A.v
B.v
C.v

[abhishek@optiplex temp]$ coq_makefile -f _CoqProject -o Makefile

[abhishek@optiplex temp]$ make -j3
make[1]: *** No rule to make target 'C.v', needed by 'C.vo'.  Stop.
make[1]: *** Waiting for unfinished jobs....
COQC A.v
COQC B.v
File "./B.v", line 1, characters 15-21:
Error: Unable to locate library Test.A.

Clearly, the coq_makefile generated Makefile invoked coqc on B.v before A.v was compiled. Is it desirable to totally ignore the dependencies if _CoqProject has nonexistent .v files?

When I removed the nonexistent C.v from _CoqProject, everything works as expected. Also unlike before, I see a COQDEP invocation on `make`

[abhishek@optiplex temp]$ cat _CoqProject  
-Q . Test

A.v
B.v

[abhishek@optiplex temp]$ coq_makefile -f _CoqProject -o Makefile

[abhishek@optiplex temp]$ make -j3 -k
COQDEP VFILES
COQC A.v
COQC B.v
[abhishek@optiplex temp]$

--

-- Abhishek

http://www.cs.cornell.edu/~aa755/