Janno (Dec 02 2020 at 13:01): Janno (Dec 02 2020 at 13:01):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?
Gaëtan Gilbert (Dec 02 2020 at 13:02):yeah I know what it is
Pierre-Marie Pédrot (Dec 02 2020 at 13:03):Linear algorithm in a tight loop?
Pierre-Marie Pédrot (Dec 02 2020 at 13:04):(I was precisely complaining in the other thread about the crazy cost induced by universe naming...)
Gaëtan Gilbert (Dec 02 2020 at 13:09):https://github.com/coq/coq/pull/13551 should fix
Pierre-Marie Pédrot (Dec 02 2020 at 13:10):@Gaëtan Gilbert that' s not what is highlighted in the trace though?
Gaëtan Gilbert (Dec 02 2020 at 13:10):actually maybe that's the wrong fix
Pierre-Marie Pédrot (Dec 02 2020 at 13:11):The problem seems to be that externalization is eagerly inventing names for the quintillion of who-the-hell-cares local universes.
Gaëtan Gilbert (Dec 02 2020 at 13:15):I'll move the name invention then
Gaëtan Gilbert (Dec 02 2020 at 13:52):https://github.com/coq/coq/pull/13552
Enrico Tassi (Dec 02 2020 at 13:56):@Gaëtan Gilbert please put these in 8.13
Gaëtan Gilbert (Dec 02 2020 at 14:03):should we put mtac2 in the bench? sure as a plugin it would fail some of the time but we ignore failures
Enrico Tassi (Dec 02 2020 at 14:12):I guess we should
Janno (Dec 02 2020 at 15:09):there is a make timing command that should run our benchmarks (after a normal make).
Gaëtan Gilbert (Dec 02 2020 at 15:11):the bench uses opam
Janno (Dec 02 2020 at 15:13):I suppose that means we need a new package or something like that?
Gaëtan Gilbert (Dec 02 2020 at 15:39):yeah
Last updated: Oct 08 2024 at 15:02 UTC