Stream: Coq devs & plugin devs

Topic: fine-grained coq bench


view this post on Zulip Jason Gross (Jan 23 2022 at 20:57):

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)

view this post on Zulip Jason Gross (Jan 23 2022 at 20:59):

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

view this post on Zulip Karl Palmskog (Jan 23 2022 at 21:02):

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?

view this post on Zulip Karl Palmskog (Jan 23 2022 at 21:03):

I think there are good ecosystem alternatives to firstorder these days though: sauto and Besson's itauto.

view this post on Zulip Jason Gross (Jan 23 2022 at 21:03):

Isn't firstorder by default firstorder auto with * (or is it just intuition that's intuition auto with *)? Does it get faster when you reduce the strength of the leaf tactic?

view this post on Zulip Karl Palmskog (Jan 23 2022 at 21:04):

unfortunately I don't work at that level usually (measure time with different leaf tactics). I tend to use firstorder, tauto, intuition mostly like black boxes...

view this post on Zulip Karl Palmskog (Jan 23 2022 at 21:06):

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: Feb 02 2023 at 13:03 UTC