The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi

I'm trying to understand what parallel proof checking (in batch mode) can and 
can't do (and why). I read 
https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html)
 and experimented a bit with one of my developments. 

From my experiments, it appears that running "make -j8 quick" and then "make 
-j8 vio2vo J=8" (coq-8.8 on a 4 cores / 8 threads CPU) does generate all .vo 
files in parallel, but there appears to be no parallelism regarding the 
proofs within the files. That is, in a development with many .v files, but 
three large files each taking about 25% of the total compilation time, I 
quickly get to the point where there are only 3 processes running.

Is this a configuration issue, or is this a limitation of the vio2vo 
conversion? If it is a limitation, is this simply not implemented or what is 
the reason?

Also, I noticed that "make vio2vo" does not generate the .glob files needed 
to run coqdoc. Is it possible to get the .glob files using parallel proof 
checking?

Best,
Christian