The Coq mailing list

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

On 25/01/2016 11:08, Frédéric Blanqui wrote:
> 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...

Yet there must be a reason for the compilation to be 30% slower while
Coq itself is only 5% slower. You didn't mention anything about the
memory of your computer; I hope you have enough memory so that 20 Coq
processes can run concurrently and do not have to be swapped out.

One thing you could try first is to use the "time" command from your
system rather than the one from your shell, so that we get the number of
major and minor pagefaults. That would give us a hint about whether your
compilation process is being I/O bound because of memory.

Then you can also tell us how large the .vo files are between 8.4 and
8.5. It might be that Coq is producing .vo files so large that it
actually brings your system down to its knees.

Finally, you might have to use "perf"-like tools to discover what the
operating system is busy doing. Indeed, while Coq is only 5% slower, the
operating system is 25% slower in your tests, so it would be interesting
to know what it is actually wasting time on.

Best regards,

Guillaume