Why is set_metas not just { evd with metas }
? https://github.com/coq/coq/blob/5db27e4dc15e0f4efd0c5707650ac1afbb42fa41/engine/evd.ml#L1134
cc @Pierre-Marie Pédrot
The latter is slow as compiled by OCaml, because its copy + set, the latter triggering a write barrier.
there is a threshold above which it should be compiled that way, but evar maps have not enough fields for that
we set_metas often enough for it to matter?
I think it was observable at some point, indeed.
Maybe less so now that we're less reliant on metas
Last updated: Nov 29 2023 at 06:01 UTC