Whenever I look at perf
profiles of Ltac2 tactics I see function names such as camlLtac2_plugin__Tac2core__anon_fn$5buser$2dcontrib$2fLtac2$2ftac2core$2eml$3a1086$2c11$2d$2d462$5d_8111
. perf
doesn't actually have any samples for this, it says it just "appears in the callchain". Is there anything I can do to get more informative function labels or generally more informative stack samples for Ltac2?
Never seen that. Are you using the +fp switch of OCaml?
Yes :(
Would I get more/better output without that?
No, it's the converse, +fp is supposed to give you meaningful backtraces.
What version of OCaml are you using?
Oh, sorry, I got it mixed up with -flambda
.
ocaml-variants.4.07.1+flambda
aha
So I'll ad +fp
and hope for the best?
it might be due to flambda mangling the function calls
but yes, try +flambda+fp, and if this doesn't work, +fp alone should.
I routinely use 4.07.1+fp and I have never seen the kind of mangled names above
You don't need the +fp
branch. Just pass --call-graph=dwarf
or --call-graph=lbr
to perf record
. (The latter is much faster, but it requires some very recent Intel processor.)
I always use --call-graph dwarf
but that doesn't help.
You are not getting call chains with it?
I am not sure what that means exactly. I get mangled and cryptic Ltac2 function names. Most other thing seem fine.
Here's an example profile: https://share.firefox.dev/3tDrptK
You can see that most Coq functions are named correctly but figuring out what part of ltac2 is responsible for the pretyping calls that take up 52% of the execution time is basically impossible because I have nothing to go on.
they're just anonymous functions
not sure but I think the format of the mangling is camlModuleName|path|to|file|ml|line|other stuff
(with separators |
replaced by $
and 2 characters (probably some kind of hash))
so for instance camlStm__anon_fn$5bstm$2fstm$2eml$3a2141$2c39$2d$2d220$5d_56560
would point to https://github.com/coq/coq/blob/fcfeb5bc45febe1a05f44a0a77b43be6b6905f35/stm/stm.ml#L2141 which does have a fun
with separators removed camlStm__anon_fn stm stm ml 2141 39 220 _56560
Oh, cool!
Let's see if I can apply this to the ltac2 functions
Yup! This is very helpful. Thanks again!
if we interprete the second number as a character count the link I gave doesn't match well, but maybe you were a few commits behind, eg https://github.com/coq/coq/blob/c6cabd1ff266a91022eb86caf4a99e89c0626430/stm/stm.ml#L2141 does have a fun
on char 39
and the $
codes are escaped characters: $ then ascii hexadecimal
2e -> . etc
so it means camlStm__anon_fn[stm/stm.ml:2141,39--220]_56560
Last updated: Oct 13 2024 at 01:02 UTC