The Coq mailing list

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

Hi,

First of all, there was a bug in my previous mail.  The vio2vo target
should be more like

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

This makes sure that not just outdated, but also missing vo files are
generated.

On 08.01.2017 18:42, Enrico Tassi wrote:
> On Fri, Jan 06, 2017 at 09:19:10PM +0100, Ralf Jung wrote:
>> 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?
> 
> There is no real good reason, it is just that when I added the target I
> could not understand coq_makefile well enough to code something smarter.
> 
> Last week I started to rewrite coq_makefile, and now I think it is much
> easier to understand what it does and extend it.  See 
> 
>   https://github.com/gares/coq/tree/feature/coq_makefile2
> 
> and in particular tools/CoqMakefile.in that is where your patch could
> land. PR welcome ;-)

Seems like I wouldn't even have to learn OCaml for this one. ;)
However, this is also a question of the desired behavior.  I can't
imagine why doing vio2vo without first updating the vio files would be
desirable, or why one would always want to re-generate all the files.
But that doesn't mean it's never desirable, it may be just a lack of
creativity on my side.  I can sure propose a PR, but I also emailed the
list here to acquire some feedback on what people think vio2vo should
do.  If it were up to me, I would get rid of vio2vo entirely and just
let "make quick" do the full job -- essentially, making it so that "make
quick J=X" is the faster "make -jX".
  But then there is this other target, checkproofs. It also depends on
make quick being run first, but it doesn't actually generate any files
so it can't really be made incremental.  If "make quick" becomes "the
fast make", then what should "make checkproofs" do?

Also, I know very little about non-Linux-Makefiles, so it is well
possible that whatever I write here breaks on macOS or Windows/MinGW or
whatever.

Finally, there's still room for improvement: In the v -> vio phase, not
all cores are fully used.  However, fixing this while still also
providing the "slow" build doesn't seem simple (or it requires a higher
level of Makefile magic than what I am able to accomplish).  Two things
would have to change for quick mode:  The .v.d files should not specify
any dependencies for the .vo files (just for .vio and whatever else),
and instead there is a generic %.vo target in the Makefile that uses the
corresponding %.vio file and has no further dependencies.  This would
mean that vio2vo scheduling is done by make, not Coq (but since PG can
do that scheduling, I assume that's fine and it doesn't have to be Coq
doing the scheduling).  It would thus be incremental just by make's
usual magic; really, the hack I proposed above is re-implementing some
of the logic that make usually takes care of. And it could use CPUs with
higher numbers of cores better, because the v -> vio and vio -> vo
phases are interleaved, so if there's not enough v -> vio jobs (because
the development does not have sufficient parallelism), some vio -> vo
jobs can already run on the spare cores. Seeing that I have 8 cores in
my laptop now (well, 4, plus hyperthreading), most of them are bored
during the v -> vio phase.
  However, this changes the entire dependency structure of the Makefile.
I wouldn't know how to also provide a "slow" target here, which has a
different dependency structure. Really, quick vs. "old" mode would have
to be a parameter of coq_makefile here, decided in advance. (Also,
coqdep would need a flag to stop emitting dependencies for the .vo files.)
  Oh, and finally, this would probably run into
<https://coq.inria.fr/bugs/show_bug.cgi?id=5223>: As final .vo files
start to appear while
v -> vio is still running, Coq would start making different choices
about importing vio vs vo files, resulting in compilation failure. Not
sure what to do about this one. Maybe Coq should prefer the vio file
over the vo file if both are in the same directory, no matter the timestamp?

Kind regards,
Ralf