Gaëtan Gilbert (Aug 21 2020 at 14:15): 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
Gaëtan Gilbert (Aug 21 2020 at 14:15):cc @Pierre-Marie Pédrot
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.
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
Gaëtan Gilbert (Aug 21 2020 at 14:27):we set_metas often enough for it to matter?
Pierre-Marie Pédrot (Aug 21 2020 at 14:31):I think it was observable at some point, indeed.
Pierre-Marie Pédrot (Aug 21 2020 at 14:31):Maybe less so now that we're less reliant on metas
Last updated: Apr 19 2024 at 02:02 UTC