Ralf Jung (Nov 16 2020 at 17:49): Ralf Jung (Nov 16 2020 at 17:49):When using the ltac profiler, shouldn't the "local" time add up to 100%? it doesn't for me, so I don't know how to interpret this...
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─wp_pures ------------------------------ 0.6% 100.0% 1 0.447s
─reshape_expr -------------------------- 0.4% 98.6% 0 0.087s
─go ------------------------------------ 0.3% 98.2% 0 0.087s
─tac ----------------------------------- 0.8% 81.2% 17 0.078s
─add_item ------------------------------ 76.3% 76.3% 0 0.084s
─wp_finish ----------------------------- 0.1% 53.9% 8 0.060s
─wp_expr_simpl ------------------------- 0.0% 48.6% 8 0.057s
─wp_expr_eval (tactic) ----------------- 0.3% 48.5% 8 0.057s
─t ------------------------------------- 0.0% 43.8% 8 0.054s
─simpl --------------------------------- 43.7% 43.7% 8 0.054s
─eapply (tac_wp_pure_no_later _ _ _ K e' 18.8% 18.8% 10 0.011s
─filter -------------------------------- 7.4% 16.0% 28 0.015s
─wp_pure_smart (tactic3) --------------- 0.8% 14.4% 1 0.064s
─open_unify (constr) (open_constr) ----- 3.7% 8.6% 213 0.001s
─iSolveTC ------------------------------ 0.1% 7.0% 9 0.009s
─typeclasses eauto (int_or_var_opt) ---- 3.8% 7.0% 9 0.009s
─unify (constr) (constr) --------------- 4.9% 4.9% 213 0.001s
─notypeclasses refine (uconstr) -------- 4.1% 4.1% 16 0.002s
─wp_value_head ------------------------- 0.3% 4.0% 8 0.003s
─eapply tac_wp_value ------------------- 3.7% 3.7% 8 0.003s
─apply AsRecV_recv --------------------- 3.2% 3.2% 4 0.007s
AFAIK, ltac backtracking does strange things with the log, but normally only in the sense that I have less time then 100%...
Also, add_item has 0 calls here, which looks strange.
Ralf Jung (Nov 16 2020 at 18:10):there is heavy backtracking going on, yeah
Ralf Jung (Nov 16 2020 at 18:11):but this is my first time using the ltac profiler so I am interpreting this all fairly naively^^
Janno (Nov 16 2020 at 18:12):You might have more luck timing things manually using https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.restart-timer
Ralf Jung (Nov 16 2020 at 18:15):hm, I think that'd help less in my concrete case as I am unsure where to even look. but this is certainly a good tool to have in the toolbox, thanks!
Last updated: Oct 01 2023 at 19:01 UTC