The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sun, Jan 08, 2017 at 10:31:29PM +0100, Ralf Jung wrote:
> 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".

Having the intermediate step is a feature to me.
The point being that having  x.vio is enough to Require x.
Sure, one typically wants to turn x.vio into x.vo, but it is good
that one can tell when compilation has reached a point where things
work again.

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

Check proofs can exploit more cores, but can't generate .vo files (in
theory it is possible, but it requires quite some coding...).

> 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).

I think that for many use cases the scheduling done by make is just fine.
The one Coq performs is optimal (if you have .aux files around) but it
really matters only for developments where at least 1 file is very slow
(you want to start with that one on one core, for example).

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

I agree, still the hope is that v->vio is fast, so wasting some cores
in that phase is not very relevant.

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

Yep, I guess we need a flag for that.

Anyway, I think this technical discussion should be either moved to
coqdev or to github.  I'd like to reach a stage where coq_makefile2
is just a replacement for coq_makefile, and then eventually improve it.

So maybe we could work on a CEP to make the user cases clear, discuss
that proposal on this venue, and finally hack the makefiles.

Best,
-- 
Enrico Tassi