The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello Guillaume.

I know what you mention. That's why I precised "when using make -j20". I 
have 24 processors on my computer. So, I don't think that it should be a 
problem to use "-j20". In a previous version of CoLoR, I had the 
following times:

j  |
--------------------
1  | 27'00"
3  | 10'47"
20|   6'45"

So, you can see that it is really important for me to use -j20...

Frédéric.

Le 25/01/2016 10:58, Guillaume Melquiond a écrit :
> 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