Stream: Coq devs & plugin devs

Topic: Printing performance regression from 8.12.1 to master


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 13:02):

yeah I know what it is

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 13:03):

Linear algorithm in a tight loop?

view this post on Zulip 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...)

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 13:09):

https://github.com/coq/coq/pull/13551 should fix

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 13:10):

@Gaëtan Gilbert that' s not what is highlighted in the trace though?

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 13:10):

actually maybe that's the wrong fix

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 13:15):

I'll move the name invention then

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 13:52):

https://github.com/coq/coq/pull/13552

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:56):

@Gaëtan Gilbert please put these in 8.13

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Dec 02 2020 at 14:12):

I guess we should

view this post on Zulip Janno (Dec 02 2020 at 15:09):

there is a make timing command that should run our benchmarks (after a normal make).

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 15:11):

the bench uses opam

view this post on Zulip Janno (Dec 02 2020 at 15:13):

I suppose that means we need a new package or something like that?

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 15:39):

yeah


Last updated: Mar 29 2024 at 07:01 UTC