Stream: Coq devs & plugin devs

Topic: uState performance


view this post on Zulip Enrico Tassi (Aug 28 2020 at 15:14):

Dear masters of the universe, after a Coq call I wrote this API
https://github.com/coq/coq/blob/911f33f0a0ff648082d329841388f59e8cecf231/engine/uState.ml#L544-L550
I'm using it in coq-elpi and I'm happy with its behavior, but the performances are ugly. Can it be implemented in a better way?
For the record, a silly coq-elpi API, like opening/closing a module, takes 0.000072s without calling demote, but 0.000746s calling it O_o (I'm calling it after every API that has an impact on the global environment)

view this post on Zulip Enrico Tassi (Aug 28 2020 at 15:15):

CC @Cyril Cohen

view this post on Zulip Enrico Tassi (Aug 28 2020 at 15:18):

Actually, that timing is with/without commenting this line

   let sigma = Evd.from_ctx (UState.demote_global_univs env (Evd.evar_universe_context sigma)) in

So I guessed the culprit is demote.


Last updated: Oct 15 2021 at 20:02 UTC