coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Coq 8.5 is out!, (continued)
- Re: [Coq-Club] Coq 8.5 is out!, Maxime Dénès, 01/22/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Enrico Tassi, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Enrico Tassi, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Jacques-Henri Jourdan, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Pierre-Marie Pédrot, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Emilio Jesús Gallego Arias, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Pierre-Marie Pédrot, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Jacques-Henri Jourdan, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Maxime Dénès, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Maxime Dénès, 01/22/2016
Archive powered by MHonArc 2.6.18.