Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.5 is out!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.5 is out!


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq 8.5 is out!
  • Date: Mon, 25 Jan 2016 13:00:15 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page