I am trying to pinpoint a performance regression in
pr_econstr_env related to printing of universes or maybe just polymorphic constants even when universes are not actually printed. 8.12.1 is working fine but master is slower by an unknown but huge factor. The problem only shows up because Mtac2 unnecessarily calls the printing function many many times so I doubt anyone else will notice this. This flamegraph excerpt should show the functions involved. I don't have a reproducible example that is easy to use for bisecting so I am wondering if anybody remembers any changes that would be relevant here?
yeah I know what it is
Linear algorithm in a tight loop?
(I was precisely complaining in the other thread about the crazy cost induced by universe naming...)
https://github.com/coq/coq/pull/13551 should fix
@Gaëtan Gilbert that' s not what is highlighted in the trace though?
actually maybe that's the wrong fix
The problem seems to be that externalization is eagerly inventing names for the quintillion of who-the-hell-cares local universes.
I'll move the name invention then
@Gaëtan Gilbert please put these in 8.13
should we put mtac2 in the bench? sure as a plugin it would fail some of the time but we ignore failures
I guess we should
there is a
make timing command that should run our benchmarks (after a normal
the bench uses opam
I suppose that means we need a new package or something like that?
Last updated: Jun 08 2023 at 04:01 UTC