Whenever I look at
perf profiles of Ltac2 tactics I see function names such as
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?
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
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
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
with separators removed
camlStm__anon_fn stm stm ml 2141 39 220 _56560
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
$ codes are escaped characters: $ then ascii hexadecimal
2e -> . etc
so it means
Last updated: Dec 07 2023 at 14:02 UTC