The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

Because the time is still spent in that tactic.  It seems obvious to me that the time spent in _expression_ evaluation should be counted as in that tactic; to say otherwise seems misleading to me.

The real question is, do we count the calls in _expression_ evaluation?  If we do then a tactic defined as `idtac` will accumulate two calls: once when it's evaluated trivially to idtac, and again when it's run.  But if we don't include the calls in _expression_ evaluation, then we end up with the problem you've encountered, where some tactics have no calls.

On Sat, Jul 25, 2020, 21:36 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

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