The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I tried Jacques-Henri's patch and, indeed, I get a total compilation 
time similar to the one of Coq 8.4pl6:

Coq 8.5 + Jacques-Henri's patch:

real    6m9.398s
user    24m25.620s
sys    1m29.282s

For completeness, I remind you the results with the other Coq versions:

Coq 8.5:

real    8m12.333s
user    32m43.505s
sys    1m43.168s

Coq 8.4pl6:

real    6m9.043s
user    31m30.582s
sys    1m23.429s

So, I think that it is worth releasing a Coq 8.5pl1 with this patch very 
quickly. :-)

Frédéric.

Le 25/01/2016 14:16, Jacques-Henri Jourdan a écrit :
> Maybe this is due to the universe algorithm. Have you tried my patch
> (included in trunk but not in 8.5 currently) ?