Stream: Elpi users & devs

Topic: Performance bottleneck in UState.demote_global_univs

Janno (Nov 12 2023 at 16:26):

I am looking at performance profiles of our uses of elpi (mostly generating definitions in the examples I am looking at) and it seems we are spending about a quarter to a third of the entire elpi execution time in UState.demote_global_univs. Is there any way this call can be avoided? We have around upwards of 10k global universes in our files.

Enrico Tassi (Nov 12 2023 at 20:34):

I've seen that already, there are two options:

• demote_blabla is re-computing something that is somehow returned by the APIs declaring constants. At least this is what @Pierre-Marie Pédrot once told me. In a way the API tells you which universes are promoted to global, and I could just use that instead of inferring this piece of info a posteriori. I did not try to do it.
• if the same elpi code does multiple definitions in a row and the definitions are kind of disjoint (like in derive you run multiple derivations, each could run alone, but you are just calling all of them one after the other), then you could try @dropunivs! (see what derive.elpi does).

The former would be nice, but I don't have the time to even look into it before end of november.

Last updated: Oct 13 2024 at 01:02 UTC