Stream: Coq devs & plugin devs

Topic: help debugging Ltac performance?


view this post on Zulip Jason Gross (Jul 27 2022 at 15:03):

I'm trying to figure out what's going wrong with https://github.com/mit-plv/fiat-crypto/pull/1350. src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v takes about twice as long to compile than it did before. Almost all the time is spent in Ltac that constructs constrs, so the Ltac profiler is not much help. I'm not really sure how to make sense of the data from perf record. (The change I made was to use transparent abstract to deduplicate reification work, so I'm guessing that either it's spending more time checking the cache (overhead would be underneath abstract/transparent_abstract), or looking up things in the cache (overhead would be underneath constr equality checking / match term with term), or maybe it's spending more time typechecking (overhead in constr:(...)) or creating / unifying / resolving evars. I don't know how to read this off the perf data, though...)
The slower version looks like
image.png
while the faster version looks like
image.png

(cc @Pierre-Marie Pédrot )

view this post on Zulip Janno (Jul 27 2022 at 15:07):

I think the second screenshot is not a perf report, is it? Is that a mistake?

view this post on Zulip Jason Gross (Jul 27 2022 at 15:18):

Oops, fixed, thanks @Janno

view this post on Zulip Janno (Jul 27 2022 at 15:24):

It's hard to say what is going on in that perf profile with all these unknown functions. I am not sure what the reason for this is. The profile should have useful names for all functions in it.

view this post on Zulip Jason Gross (Jul 27 2022 at 15:36):

Maybe this version of Coq or OCaml was somehow compiled without complete debug info?

view this post on Zulip Jason Gross (Jul 27 2022 at 15:44):

objdump --syms $(which coqc) lists a bunch of things, but there are no symbols for ocamlc / ocamlopt

view this post on Zulip Jason Gross (Jul 27 2022 at 15:44):

(This is on Arch)

view this post on Zulip Guillaume Melquiond (Jul 27 2022 at 15:56):

This looks like bogus stack traces. Did you forget to pass --call-graph=dwarf to perf record?

view this post on Zulip Jason Gross (Jul 27 2022 at 22:09):

Oh, I wasn't aware that I need to pass --call-graph=dwarf. I was just doing perf record -g

view this post on Zulip Jason Gross (Jul 27 2022 at 23:15):

--call-graph=dwarf does not help
image.png

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2022 at 16:52):

@Jason Gross you need to use a version of the OCaml compiler with the fp flag for the callstack to be meaningful.

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2022 at 16:52):

I personally use ocaml-variants.4.09.1+fp on a daily basis.


Last updated: Feb 05 2023 at 20:03 UTC