Stream: Coq devs & plugin devs

Topic: set_metas with???


view this post on Zulip Gaëtan Gilbert (Aug 21 2020 at 14:15):

Why is set_metas not just { evd with metas }? https://github.com/coq/coq/blob/5db27e4dc15e0f4efd0c5707650ac1afbb42fa41/engine/evd.ml#L1134

view this post on Zulip Gaëtan Gilbert (Aug 21 2020 at 14:15):

cc @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Aug 21 2020 at 14:21):

The latter is slow as compiled by OCaml, because its copy + set, the latter triggering a write barrier.

view this post on Zulip Pierre-Marie Pédrot (Aug 21 2020 at 14:21):

there is a threshold above which it should be compiled that way, but evar maps have not enough fields for that

view this post on Zulip Gaëtan Gilbert (Aug 21 2020 at 14:27):

we set_metas often enough for it to matter?

view this post on Zulip Pierre-Marie Pédrot (Aug 21 2020 at 14:31):

I think it was observable at some point, indeed.

view this post on Zulip Pierre-Marie Pédrot (Aug 21 2020 at 14:31):

Maybe less so now that we're less reliant on metas


Last updated: Oct 21 2021 at 21:03 UTC