Enrico Tassi (Aug 28 2020 at 15:14): 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)
Enrico Tassi (Aug 28 2020 at 15:15):CC @Cyril Cohen
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: Apr 20 2024 at 00:02 UTC