The Coq mailing list

[David Holland <dholland-coq AT netbsd.org>]

On Fri, Jul 17, 2020 at 06:24:31PM -0700, Abhishek Anand wrote:
 > I want to avoid ever having to do clean builds (`make clean`) and still
 > ensure soundness of the build.
 > [...]
 > 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`.

Don't forget to also delete leftover .foo.aux files.

That said, there are always cases where you have to make clean,
because make relies on timestamps to detect when files have been
changed and timestamps can get screwed up. For example, if you
accidentally set your clock forward a week and work for a while before
fixing it, you'll likely be left with build products dated in the
future that won't be rebuilt properly.

Timestamps also don't (normally) cover all the possible things that
might change your build; e.g. when you update Coq you need to make
clean, and you generally want or need to if you change build settings.

And if the storage you're working from runs over a network (including
most cases of being shared inside and outside a VM) you can get
various problems arising from clock skew, and if you access such
storage from two or more places, sometimes cache (in)consistency as
well. (The latter is particularly bad with NFS because there are no
consistency guarantees at all, just some ad hoc timeouts, and
timestamp changes don't necessarily propagate at the same time as file
contents changes.)

Other than things like that though... make is supposed to give you
consistent builds, and coq_makefile is supposed to produce correct
makefiles, so if it doesn't work it's a bug in (most likely)
coq_makefile or (quite unlikely) make or the OS.

-- 
David A. Holland
dholland AT netbsd.org