Would it be possible to get coq bench to report (or at least make available) how much time is spent in each component? e.g., how much time is spent in parsing vs pretyping vs internalization vs unification vs conversion vs universe checking vs substitution vs evar map traversal vs vm vs native vs module functor substitution vs Ltac interpretation vs other Ltac (cc @ppedrot)
Relatedly, I wonder if it'd be useful to have a mode of coq-bench that turns on
Ltac Profiling for all files, and aggregates the Ltac profiling results across files of each development, maybe even across developments. This might give a sense of which tactics it makes the most sense to performance engineer
anecdotally slowest for me has been
firstorder. I don't think there are plans to work on it, though, I think PMP considered it unsalvageable?
I think there are good ecosystem alternatives to
firstorder these days though:
sauto and Besson's
firstorder by default
firstorder auto with * (or is it just
intuition auto with *)? Does it get faster when you reduce the strength of the leaf tactic?
unfortunately I don't work at that level usually (measure time with different leaf tactics). I tend to use
intuition mostly like black boxes...
the selling point of
itauto in my mind was to have to care even less about choice of leaf tactic and what a tactic really expands to under the hood...
Last updated: Jun 09 2023 at 07:01 UTC