The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi,

Another thing that shows from time to time in my Coq profiling is the
directory caching code.

This could explain the increase in system time that Guillaume was
talking about.

[So far universe checking is almost always on top of the profiles, in
 particular HMap.find seems like a bottleneck, JH patch makes it better
 but not to go away. Unfortunately this is just a guess as I can't trust
 my profiling data yet]

Emilio

Pierre-Marie Pédrot 
<pierre-marie.pedrot AT inria.fr>
 writes:

> On 25/01/2016 14:16, Jacques-Henri Jourdan wrote:
>> Maybe this is due to the universe algorithm. Have you tried my patch
>> (included in trunk but not in 8.5 currently) ?
>
> Quick perfing suggests there may be a ~15% improvement with your patch,
> but this would need testing to be confirmed.
>
> @Frédéric: are there precise lines of code that got worse between 8.4
> and 8.5 (let's say in rpo.v)? If so, could you give them so I can try to
> guess what changed between the two?
>
> PMP