Zulip Chat Archive

Stream: general

Topic: how expensive is rw?


Kenny Lau (May 30 2018 at 23:05):

a profiler for a long proof I just typed:

elaboration: tactic execution took 6.66s
num. allocated objects:  20027
num. allocated closures: 20050
 6658ms   100.0%   tactic.istep._lambda_1
 6658ms   100.0%   _interaction._lambda_2
 6658ms   100.0%   tactic.istep
 6658ms   100.0%   tactic.step
 6658ms   100.0%   scope_trace
 6548ms    98.3%   tactic.solve1
 4617ms    69.3%   interaction_monad.monad._lambda_9
 4612ms    69.3%   tactic.interactive.propagate_tags
 4131ms    62.0%   rw_core
 4093ms    61.5%   _private.3132620493.rw_goal._lambda_4
 4093ms    61.5%   interactive.loc.apply
 4092ms    61.5%   interaction_monad.orelse'
 4092ms    61.5%   _private.3132620493.rw_goal._lambda_2
 4069ms    61.1%   tactic.rewrite_target
 4009ms    60.2%   tactic.rewrite
 3972ms    59.7%   tactic.rewrite_core
 1494ms    22.4%   tactic.ac_refl
 1489ms    22.4%   cc_state.internalize
  524ms     7.9%   tactic.interactive.apply._lambda_1

Kenny Lau (May 30 2018 at 23:06):

Highlight:

 3972ms    59.7%   tactic.rewrite_core
 1494ms    22.4%   tactic.ac_refl

Mario Carneiro (May 30 2018 at 23:16):

what was the rewrite

Kenny Lau (May 30 2018 at 23:16):

it was 100 rewrites

Kenny Lau (May 30 2018 at 23:32):

another highlight:

Kenny Lau (May 30 2018 at 23:32):

 6548ms    98.3%   tactic.solve1
 4617ms    69.3%   interaction_monad.monad._lambda_9

Kenny Lau (May 30 2018 at 23:32):

what is so expensive about focussing on a goal?

Kenny Lau (May 30 2018 at 23:33):

 1489ms    22.4%   cc_state.internalize
  524ms     7.9%   tactic.interactive.apply._lambda_1

Kenny Lau (May 31 2018 at 02:27):

After some optimizations (heavily cutting down the workload of rw):

elaboration: tactic execution took 3.65s
num. allocated objects:  9569
num. allocated closures: 7495
 3653ms   100.0%   tactic.istep
 3653ms   100.0%   scope_trace
 3653ms   100.0%   tactic.step
 3653ms   100.0%   _interaction._lambda_2
 3653ms   100.0%   tactic.istep._lambda_1
 3554ms    97.3%   tactic.solve1
 2271ms    62.2%   interaction_monad.monad._lambda_9
 1792ms    49.1%   interaction_monad_orelse
 1584ms    43.4%   tactic.interactive.convert
 1581ms    43.3%   tactic.interactive.congr'
 1581ms    43.3%   tactic.focus1
 1579ms    43.2%   tactic.interactive.congr'._main._lambda_1
 1548ms    42.4%   tactic.all_goals
 1548ms    42.4%   _private.3864167971.all_goals_core._main._lambda_2
 1548ms    42.4%   all_goals_core
 1241ms    34.0%   tactic.interactive.propagate_tags
 1127ms    30.9%   tactic.apply_core

Kenny Lau (May 31 2018 at 02:27):

I'm still surprised that solve1 took the most time

Kenny Lau (May 31 2018 at 02:27):

I thought solve1 is the most inexpensive tactic

Sebastian Ullrich (May 31 2018 at 07:00):

This doesn't have to mean that solve1 is slow, more probably it means that you have multiple calls to it, and not all of them call _lambda_9 next.

Sebastian Ullrich (May 31 2018 at 07:01):

Basically, the profile trace isn't all that useful right now

Gabriel Ebner (May 31 2018 at 07:29):

The reason for the comparatively large runtime of solve1 is not that it is called often, but that it calls the tactic you give it as an argument. That is, when you have begin { my_tactic } end, then my_tactic is executed by solve1 and hence the cumulative runtime of solve1 includes the runtime of my_tactic.


Last updated: Dec 20 2023 at 11:08 UTC