Stream: Coq users

Topic: Ltac Profiling: why so much local time

Fabian Kunze (Nov 23 2020 at 20:16):

I used Ltac profiling and can't explain myself the result.
Does anyone have an Idea how this tactic can have 64.3 % _local_ time? Shouldn't all of the work be inside of the different sub-tactics?

Ltac tacMain :=
   t1; repeat (repeat t2;t3);
  try t4.

I get then feeling that the repeat causes the time to get "assigned" to the main tactic.

Fabian Kunze (Nov 23 2020 at 20:17):

For the record: wrapping everything into "once" did not change anything, so I don;t think it's backtracking.

Pierre-Marie Pédrot (Nov 23 2020 at 20:55):

repeat calls progress, which can be quite costly

Pierre-Marie Pédrot (Nov 23 2020 at 20:56):

if you run a low-level profiler, you might be able to see it.

Pierre-Marie Pédrot (Nov 23 2020 at 20:56):

(or maybe Ltac profile is confused on your particular example and is giving you a garbage profile?)

Fabian Kunze (Nov 24 2020 at 10:00):

Oh, of course, that is something to think about.
What do you mean by "low level profiler"? This is not a tool shiped with cow, is it? so it's really profiling the ocaml?

Fabian Kunze (Nov 24 2020 at 10:18):

This should be a drop-in replacement without progress check:

Tactic Notation (at level 3) "repeat_noProgressCheck" tactic3(t) :=
  let rec loop := (tryif t then loop else idtac) in loop.

Fabian Kunze (Nov 24 2020 at 10:28):

well, if one does want to fail this tactical if nothing happened, this might be better:

Tactic Notation (at level 3) "repeat_noProgressCheck" tactic3(t) :=
  let rec loop := (tryif t then loop else idtac) in t;loop.

Paolo Giarrusso (Nov 24 2020 at 11:59):

so t is supposed to contain an implied progress (aka fail if it doesn’t progress?), else your tactical will loop

Paolo Giarrusso (Nov 24 2020 at 12:00):

(e.g. repeat_noProgressCheck idtac should loop)

Fabian Kunze (Nov 24 2020 at 12:35):

Yes, my new semantics is "repeat until fail", not "repeat until fail or noprogress"

Fabian Kunze (Nov 24 2020 at 12:36):

I used repeat very deep in a custom term transformation tactic and it was more than half the time spend inside the repeat, althought I know in my use case when progress occured and when not from within.

Fabian Kunze (Nov 24 2020 at 12:36):

and the second version, that executes t at least once, allows for the proper nesting of such "self-detect progress" tactics.

Fabian Kunze (Nov 24 2020 at 12:37):

with this nicer name, I even get syntax highlighting in vscoq:

Tactic Notation (at level 3) "repeat'" tactic3(t) :=
  idtac;let rec loop := (tryif t then loop else idtac) in t;loop.

Pierre-Marie Pédrot (Nov 24 2020 at 12:37):

re: profiling, I personally use the linux perf tool utility to profile Coq runs

Pierre-Marie Pédrot (Nov 24 2020 at 12:38):

Note that the code of progress could be made more clever.

Pierre-Marie Pédrot (Nov 24 2020 at 12:39):

if your problem does come from the cost of progress, we could try to see whether a slightly better heuristic would help

Fabian Kunze (Nov 24 2020 at 12:42):

In my use case, I have the "self-computed progress via fail" almost for free.
Furthermore, I use evars a lot. Would your proposed, more-clever implementation detect that e.g. that using transitivity;[reflexivity| ] on the goal "7 <= ?x" does not do progress?

Pierre-Marie Pédrot (Nov 24 2020 at 12:43):

this is not a problematic instance of progress though?

Pierre-Marie Pédrot (Nov 24 2020 at 12:43):

except maybe if you have a gazillion of hypotheses

Fabian Kunze (Nov 24 2020 at 12:44):

I myself am not quite sure what the current answer to this question is and whether I use this "feature", so maybe I'll just leave this pandora's box closed.

Pierre-Marie Pédrot (Nov 24 2020 at 12:45):

I am not proposing to change the observational behaviour of progress, just its implementation.

Fabian Kunze (Nov 24 2020 at 12:51):

Sorry, I did not want to imply that.
I'm already happy with the don't-use-progress-alternative. As the terms I used repeat on are quite large I'm not sure if the improvement would help me here.

Fabian Kunze (Nov 24 2020 at 15:33):

Oha, the problem was not with the "progress", but it seems that tactic evaluation "unfolded" part of tacMain.
By wrapping the body of tacMain into a lazymatch goal with |- _ => .. end, all the time is properly assigned to t1 :sad:

Jason Gross (Nov 25 2020 at 15:46):

What's the body of t1? (Does it start with match, lazymatch, or let?) I don't entirely understand why wrapping tacMain in lazymatch fixes things (it has something to do with the difference between tactic evaluation and execution), but I think a more robust fix, in some sense, would be sticking idtac; at the beginning of the body of t1. The thing to realize here is that Ltac has two evaluation phases, and for reasons I don't quite recall, sometimes the code run during the first evaluation phase gets associated with the parent tactic. (AIUI, this is not a problem with the profiler per se, and the issue can already be observed in the backtrace associated to a tactic failure.)

Fabian Kunze (Nov 25 2020 at 15:55):

I have to look again. One thing to mention is that the tactic tacMain is passed around as an argument, maybe that is related/

Fabian Kunze (Nov 25 2020 at 16:05):

I can't reconstruct it, but using idtac for thunks makes the log a lot cleaner, thanks.
I think i had a configurable extendableTac t whose argument t was intended to be of "type" unit -> ltac, and i called t inside extendableTac by writing t ().

The argument I passed for t was of form fun _ => (match goal with $pattern => tacMain end;moreTac).

Fabian Kunze (Nov 25 2020 at 16:06):

t1 was someWrapperTac ltac:(fun _ => someArgumentTac)., and someWrapperTac is lazymatch goal on head

Fabian Kunze (Nov 25 2020 at 16:08):

I sprinkled a lot of lambda-lifting without understanding where it actually is needed.

So basically, instead of ltac:(fun _ => someTac) to not evaluate a tactic when supplied as argument, one should just pass idtac;someTac?

Last updated: Oct 13 2024 at 01:02 UTC