The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/01/2016 10:35, Frédéric Blanqui wrote:
> Hello.
> 
> Thanks for the Coq developers for having found a way to solve my
> problems quickly.
> 
> This new release of Coq is a great job anyway!
> 
> I will release a new version of CoLoR for Coq 8.5 very quickly.
> 
> However, I would like to mention that the compilation time (not using
> Enrico's new compilation procedure) increased by 33% between Coq 8.4pl6
> and Coq 8.5 when using make -j20!... :-(
> 
> make -j20 with Coq 8.4pl6 gives:
> real    6m9.043s
> user    31m30.582s
> sys    1m23.429s
> 
> make -j20 with Coq 8.5 gives:
> real    8m12.333s
> user    32m43.505s
> sys    1m43.168s

Be careful there. Notice that the operating system is telling you that
Coq itself (the "user" value) is only 5% slower. That is bad, but not
that bad.

My guess is that your computer is not able to run 20 instances of Coq
concurrently: it has neither the processing power nor the memory to
handle them. (Or are you compiling CoLoR on a powerful server?) So the
values you get are not that helpful.

As a rule of thumb, I never try to run more Coq instances than I have
hardware threads nor memory gigabytes; so I usually end up running at
"-j3" on my own computer. It would be interesting to know which slowdown
you get when you are using a more sensible value for "-j".

(Contrarily to common belief, increasing the "-j" value does not always
speed up the compilation process. After a point, increasing it will
actually make the compilation process slower!)

Best regards,

Guillaume