Stream: Coq users

Topic: Ltac profiler


view this post on Zulip 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

view this post on Zulip Fabian Kunze (Nov 16 2020 at 17:53):

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.

view this post on Zulip Ralf Jung (Nov 16 2020 at 18:10):

there is heavy backtracking going on, yeah

view this post on Zulip 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^^

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC