The Coq mailing list

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

Hi,

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

Ah, that's interesting -- so it can be more parallel because it doesn't
have to produce the .vo files.

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

Oh, I didn't know it does that. That's cool.

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

In our developments, the v -> vio phase and vio -> vo phase both take
about the same time. So I think using the cores better in the first
phase would be very noticeable.

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

All right. I'll first follow up in the aforementioned bugreport, as
that's a prerequisite (and would be helpful otherwise).
Does "make vio2vo incremental and make it call 'make quick'" also need a
CEP, or just a PR?

Kind regards,
Ralf