The Coq mailing list

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

Suppose we have a directory X containing Coq files, possibly inside nested directories.
Suppose we have a standard Coq build system: all the Coq (.v) files are listed in X/_CoqProject, which is used to produce X/Makefile and then make is used to build all the .v files.
Suppose all Require Imports in the Coq files use fully qualified logical names.
During the normal development, files/directories may be added/updated/removed in X.
I want to avoid ever having to do clean builds (`make clean`) and still ensure soundness of the build.
The main reason is to save time: coq repos can be huge and proofs can take a lot of time to build.
By soundness, I mean that the build result (set of .vo files) is equivalent to the result of `make clean; git clean -xdf; coq_makefile ..; make`.
Below is an approach that I think works. I'd appreciate counterexamples or arguments why this is correct:
1) delete every .vo, .vio, .vos, .glob file that does not correspond to a .v file in X/_CoqProject.
2) reinvoke coq_makefile on X/_CoqProject to regenerate X/Makefile
3) `make`.

Thanks,

-- Abhishek

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