The Coq mailing list

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

Sorry. I wasn't trying to argue one way or the other.  I was just
expressing some surprise about that way of measuring.  As you know,
it's almost never the case that one wants a tactic that evaluates as a
pure tactic expression, although in most usages it doesn't matter.  So I
have no problem using "count 0" as an indicator that I need to insert
"idtac;" at the beginning of that tactic definition.

But, I still don't know what the local column is about.  I now have
seen tests where it can't possibly mean the time spent in the tactic
excluding its callees, because then the local column would not sum to
well over 100%, which it can do.  It does seem that local is always <=
total, but sometimes it is just slightly <, and other times it is very
much <.


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

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