The Coq mailing list

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

The 'use_node' tactic is a tactic expression (no ';' sequence), so I can
understand why (but did not anticipate that) its count would be 0
according to the info you provided.  But it is still counted with
respect to local and total timing, according to the output.  If as a
tactic expression it is evaluated and not counted, why then isn't its
evaulated form counted directly by its parent tactics in the call chain?

Regardless, I will stick an "idtac;" at the start of each 0-counted
tactic that I want correct call counts for (which is all of them).

On Sat, 25 Jul 2020 20:34:21 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> What's the definition of `use_node`?  Note that the profiler does not
> count calls to tactics which are run during tactic expression
> evaluation, only during tactic running time.  Consider, for example:
> Ltac foo _ := idtac.
> Ltac bar := let __ := match goal with _ => foo () end in
>             idtac.
> Ltac baz := bar.
> Ltac qux := idtac; baz.
> 
> Goal True.
>   Set Ltac Profiling.
>   qux.
>   Show Ltac Profile CutOff 0.
>   (* total time:      0.000s
> 
>  tactic                                   local  total   calls
> max
> ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
> ─qux -----------------------------------  32.8% 100.0%       1
> 0.000s ─baz -----------------------------------  12.1%  65.5%       0
>    0.000s ─bar -----------------------------------  50.0%  55.2%
>  1    0.000s ─foo -----------------------------------   5.2%   5.2%
>     0    0.000s
> 
>  tactic                                   local  total   calls
> max
> ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
> ─qux -----------------------------------  32.8% 100.0%       1
> 0.000s ├─baz ---------------------------------  12.1%  65.5%       0
>   0.000s │└bar ---------------------------------  48.3%  53.4%
> 0    0.000s │└foo ---------------------------------   5.2%   5.2%
>   0    0.000s └─bar ---------------------------------   1.7%   1.7%
>     1    0.000s
> 
> *)
> 
> The way to interpret this is that, during tactic expression evaluation
> phase, baz calls bar which calls foo, and none of these are counted as
> calls (if they were, we'd end up double-counting almost all tactics).
> After tactic expression evaluation phase, the remaining tactic to run
> is "idtac" under "bar", so we get "bar" as a direct descendent of
> "qux" with one call.
> 
> On Sat, Jul 25, 2020 at 2:46 PM jonikelee AT gmail.com
> <jonikelee AT gmail.com> wrote:
> 
> > 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
> >