The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Just an opinion: two of my developments make intensive use of finite sets, not so much of maps. But one this I have noticed when porting such developments to Coq 8.4 was that the compilation process become much slower, when compared to Coq 8.3. I think that this may be related with modifications on the type classes mechanism that were added in Coq 8.4.  But I am not the right person to give a perfect clear answer about that!

It's unclear what caused performance losses in the v8.4 release. However, our experiment with the trunk showed that tweaking the gc parameters recovered performance on par with v8.3. This will eventually be ported to the v8.3 and v8.4 branches so that we can compare, so stay tuned. But anyway, the slowdown in v8.4 may just have been about big persistent datastructures filling the minor heap.