coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq 8.5 is out!
- Date: Mon, 25 Jan 2016 11:08:33 +0100
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.Be careful there. Notice that the operating system is telling you that
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
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
- [Coq-Club] Coq 8.5 is out!, Maxime Dénès, 01/22/2016
- Re: [Coq-Club] Coq 8.5 is out!, John Wiegley, 01/22/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/22/2016
- Re: [Coq-Club] Coq 8.5 is out!, Hugo Herbelin, 01/22/2016
- 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!, 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!, Maxime Dénès, 01/22/2016
- Re: [Coq-Club] Coq 8.5 is out!, Hugo Herbelin, 01/22/2016
Archive powered by MHonArc 2.6.18.