The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

Would it make any sense to have "incremental" vio2vo?  What I mean by
this is that it should only check and generate those vo files that
actually need updating.  Currently, if I want to check that my entire
development compiles by doing "make quick -j4 ; make vio2vo J=4", it
will always re-check all the proofs.  That's rather silly, and a
significant drawback compared to plain "make -j4".

To demonstrate what I mean, I implemented incremental vio2vo via
Makefile hackery, see
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/Makefile#L27> and
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/awk.Makefile>. When
patched, the vio2vo target in the Makefile.coq looks as follows:

> vio2vo:
>       @make -j $(J) quick
>       @VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do if [ "$$(echo 
> "$$file" | sed "s/\.vio/.vo/")" -ot "$$file" ]; then echo -n "$$file "; fi; 
> done); \
>        echo "VIO2VO: $$VIOFILES"; \
>        if [ -n "$$VIOFILES" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) 
> -schedule-vio2vo $(J) $$VIOFILES; fi

Instead of passing all the vio files to schedue-vio2vo, this first
filters the list to only keep files where the vo file is older than the
vio file. (It also turns out Coq doesn't like an empty list of vio
files, so this needs a special case.) Furthermore, I was tired of typing
"make quick && make vio2vo", so I made vio2vo also call quick with the
appropriate number of parallel jobs. (Currently this will misbehave if J
is not set, but oh well.)

Now I just do "make vio2vo J=4", and the entire development is checked
incrementally. If PG already checked and compiled some files (with the
"make quick + vio2vo in background" mode), those will also be used
instead of being overwritten.

However, I don't know very much about the internals of the vio2vo
machinery, so I'm not entirely sure if this approach even makes sense.
Can this cause trouble by mixing vo files from different "runs" of
vio2vo? Is there any good reason "make vio2vo" is *not* incremental?

Kind regards,
Ralf