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.
For the record: wrapping everything into "once" did not change anything, so I don;t think it's backtracking.
progress, which can be quite costly
if you run a low-level profiler, you might be able to see it.
(or maybe Ltac profile is confused on your particular example and is giving you a garbage profile?)
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?
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.
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.
t is supposed to contain an implied
progress (aka fail if it doesn’t progress?), else your tactical will loop
repeat_noProgressCheck idtac should loop)
Yes, my new semantics is "repeat until fail", not "repeat until fail or noprogress"
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.
and the second version, that executes t at least once, allows for the proper nesting of such "self-detect progress" tactics.
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.
re: profiling, I personally use the linux perf tool utility to profile Coq runs
Note that the code of progress could be made more clever.
if your problem does come from the cost of progress, we could try to see whether a slightly better heuristic would help
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?
this is not a problematic instance of progress though?
except maybe if you have a gazillion of hypotheses
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.
I am not proposing to change the observational behaviour of progress, just its implementation.
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.
Oha, the problem was not with the "progress", but it seems that tactic evaluation "unfolded" part of
By wrapping the body of
tacMain into a
lazymatch goal with |- _ => .. end, all the time is properly assigned to
What's the body of
t1? (Does it start with
let?) I don't entirely understand why wrapping
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.)
I have to look again. One thing to mention is that the tactic tacMain is passed around as an argument, maybe that is related/
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
extendableTac by writing
The argument I passed for
t was of form
fun _ => (match goal with $pattern => tacMain end;moreTac).
someWrapperTac ltac:(fun _ => someArgumentTac)., and someWrapperTac is
lazymatch goal on head
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
Last updated: Sep 30 2023 at 05:01 UTC