The Coq mailing list

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

On 25/01/2016 11:37, Frédéric Blanqui wrote:
> Hi Guillaume.
> 
> With /usr/bin/time make -j20, I get:
> 
> 2017.92user 108.62system 8:14.59elapsed 429%CPU (0avgtext+0avgdata
> 1850172maxresident)k
> 0inputs+607752outputs (0major+12904377minor)pagefaults 0swaps
> 
> I don't know how to interpret all this. Does this answer your questions?

Yes and no. At the very least, it tells us that memory is not an issue,
since you never had any major pagefault. But it does not tell us why the
whole compilation process got much slower while Coq itself did not. The
number of outputs seems quite large, but without a comparison point, it
is hard to tell.

> 6:
> real    9m33.979s
> user    28m0.672s
> sys    1m17.952s
> 
> 20:
> real    8m12.333s
> user    32m43.505s
> sys    1m43.168s

Notice how the system is somehow getting swamped. You seem to have gone
past the point where increasing the number of concurrent processes
actually makes the system slower, since the "user" and "system" times
are getting much higher than needed. But I have no idea what part of the
operating system is causing a bottleneck.

Best regards,

Guillaume