Stream: Coq devs & plugin devs

Topic: Cryptic Ltac2 function names in `perf` output


view this post on Zulip Janno (Mar 19 2021 at 15:56):

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?

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 16:54):

Never seen that. Are you using the +fp switch of OCaml?

view this post on Zulip Janno (Mar 19 2021 at 16:57):

Yes :(

view this post on Zulip Janno (Mar 19 2021 at 16:57):

Would I get more/better output without that?

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 16:58):

No, it's the converse, +fp is supposed to give you meaningful backtraces.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 16:58):

What version of OCaml are you using?

view this post on Zulip Janno (Mar 19 2021 at 16:59):

Oh, sorry, I got it mixed up with -flambda.

view this post on Zulip Janno (Mar 19 2021 at 16:59):

ocaml-variants.4.07.1+flambda

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 16:59):

aha

view this post on Zulip Janno (Mar 19 2021 at 16:59):

So I'll ad +fp and hope for the best?

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 16:59):

it might be due to flambda mangling the function calls

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 17:00):

but yes, try +flambda+fp, and if this doesn't work, +fp alone should.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 17:00):

I routinely use 4.07.1+fp and I have never seen the kind of mangled names above

view this post on Zulip Guillaume Melquiond (Mar 19 2021 at 17:11):

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.)

view this post on Zulip Janno (Mar 19 2021 at 17:27):

I always use --call-graph dwarf but that doesn't help.

view this post on Zulip Guillaume Melquiond (Mar 19 2021 at 17:28):

You are not getting call chains with it?

view this post on Zulip Janno (Mar 19 2021 at 17:33):

I am not sure what that means exactly. I get mangled and cryptic Ltac2 function names. Most other thing seem fine.

view this post on Zulip Janno (Mar 19 2021 at 17:33):

Here's an example profile: https://share.firefox.dev/3tDrptK

view this post on Zulip Janno (Mar 19 2021 at 17:35):

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.

view this post on Zulip Gaëtan Gilbert (Mar 19 2021 at 17:36):

they're just anonymous functions

view this post on Zulip Gaëtan Gilbert (Mar 19 2021 at 17:38):

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))

view this post on Zulip Gaëtan Gilbert (Mar 19 2021 at 17:40):

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

view this post on Zulip Janno (Mar 19 2021 at 17:41):

Oh, cool!

view this post on Zulip Janno (Mar 19 2021 at 17:42):

Let's see if I can apply this to the ltac2 functions

view this post on Zulip Janno (Mar 19 2021 at 17:43):

Yup! This is very helpful. Thanks again!

view this post on Zulip Gaëtan Gilbert (Mar 19 2021 at 17:44):

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

view this post on Zulip Gaëtan Gilbert (Mar 19 2021 at 17:59):

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 15 2021 at 20:02 UTC