Note that this implementation only puts the FrLtac frames, not the ones of anon functions.
This is especially impactful for recursion as Ltac2 rec bla binders := ... becomes Ltac2 bla binders := let rec bla binders := ... in bla binders so only the top call gets a frame, and with profiling only the top call produces overhead.
We should expect that adding frames for anonymous functions / recursive calls would be significantly worse than the current results.
ie https://github.com/SkySkimmer/coq-ltac2-compiler/issues/8
On bug_10107.v:
Note that this implementation only puts the FrLtac frames, not the ones of anon functions.
This is especially impactful for recursion as
Ltac2 rec bla binders := ...becomesLtac2 bla binders := let rec bla binders := ... in bla bindersso only the top call gets a frame, and with profiling only the top call produces overhead.We should expect that adding frames for anonymous functions / recursive calls would be significantly worse than the current results.