The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Another guess : it seems like most of the overhead is spent on IO. Have
you tried to deactivate native compilation, that can lead to quite a lot
of IOs ?

Le 26/01/2016 13:41, Pierre-Marie Pédrot a écrit :
> On 26/01/2016 09:19, Frédéric Blanqui wrote:
>> I tried Jacques-Henri's patch and, indeed, I get a total compilation
>> time similar to the one of Coq 8.4pl6:
> That's still somehow bad, because as 8.5 already should be quicker than
> 8.4, the universe patch should therefore really speed things up. It
> means we have a complexity regression somewhere, although it may be
> quite diffuse.
>
> PMP
>

Attachment: signature.asc
Description: OpenPGP digital signature