The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This will be fixed in Coq 8.13, and is already fixed in master; see https://github.com/coq/coq/pull/12427

On Tue, Aug 18, 2020, 02:35 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks. I found this non-transient timestamp-related issue, where if a file older than the last coqdep invocation is added to _CoqProject, coqdep is not reinvoked, leading to unsould incremental builds:

[abhishek@optiplex temp]$ ls -lrt
total 8
-rw-r--r-- 1 abhishek abhishek  0 Aug 17 22:32 A.v
-rw-r--r-- 1 abhishek abhishek 14 Aug 17 23:26 _CoqProject
-rw-r--r-- 1 abhishek abhishek 23 Aug 17 23:27 B.v
[abhishek@optiplex temp]$ cat _CoqProject  
-R . test
A.v
[abhishek@optiplex temp]$ coq_makefile -f _CoqProject -o Makefile
[abhishek@optiplex temp]$ make
COQDEP VFILES
COQC A.v
[abhishek@optiplex temp]$ echo "B.v" >> _CoqProject  

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

[abhishek@optiplex temp]$ rm A.vo
[abhishek@optiplex temp]$ make B.vo
coq_makefile -f _CoqProject -o Makefile
COQC B.v
File "./B.v", line 1, characters 15-21:
Error: Unable to locate library test.A.

make: *** [Makefile:678: B.vo] Error 1

[abhishek@optiplex temp]$ touch B.v
[abhishek@optiplex temp]$ make B.vo
COQDEP VFILES
COQC A.v
COQC B.v

A workaround is to also delete .Makefile.d (coqdep output) whenever _CoqProject is updated.

-- Abhishek

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

On Sat, Jul 18, 2020 at 5:32 PM David Holland <dholland-coq AT netbsd.org> wrote:

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