The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Have you thought about using IBM's ClearCase for this purpose?  One of
its many features is the ability to do sound incremental builds without
needing clean rules - it does so by keeping track of which object files
are modified by which build rules.  It's considerably more
sophisticated, as it also has rsync-like dedup capabilities and
concurrent build control, and is a versioned file system.

On Fri, 17 Jul 2020 18:24:31 -0700
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> 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/