The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I am perhaps not interpreting Ltac Profiling output correctly, but
having 0 for calls below seems like it must be a bug, since either
use_node must have been called at least once, or it must have calls
within it to have a very different local vs. total percentage:

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─tac -----------------------------------   0.6%  82.2%   41833   11.316s
─force refine (uconstr) by (tactic1) ---   0.0%  57.5%     148   11.332s
─use_node ------------------------------   0.0%  56.4%       0   23.650s
...

Is this a bug?  If not, what is the proper interpreation of the calls
column?  Or, for that matter, all columns?

My probably incorrect interpretation is that "local" refers to the
particular tactic excluding any others it calls, while "total" includes
others it calls. And calls is the total number of times it runs.  And
max is the maximal amount of time of any single call, including sub
calls.  This makes sense except for calls = 0 cases, of which I have
several.  My alternate interpretation of calls would be that it is the
total number of calls the tactic makes (subcalls), but that cannot be 0
unless that tactic's local and total are the same (or very close).  I'm
also assuming that the top "tac" line is the total for all tactics.

Note that the refman is silent about the interpretation of the output,
but its examples do show cases where calls=0.  And in those cases local
and total are very close (so perhaps my alternate interpretation of
calls is correct, and the total-local difference is just the Ltac call
overhead of the tactic itself?).

BTW: this is in the tagged 8.12 build as of yesterday, where
supposedly the longstanding Ltac Profiling shortcoming vs.
multi-success backtracking tactics has been fixed.  I had previously
not paid close attention to anomalies in the Ltac Profiling output
because of that shortcoming.

Thanks,
Jonathan