Evaluating the relative performance of two tactics

Stream: new members

[Louis Cabarion]

What is the correct way to compare the performance of two different tactics on the same example?

I’ve tried using the setup shown in the #mwe below, but I’m having trouble reconciling the numbers reported by #count_heartbeats in and those from trace.profiler true combined with trace.profiler.useHeartbeats true. The results seem to differ significantly.

Given these results, is it correct to interpret that in this specific case aesop is approximately 56% slower than rfl (110/71), 46% slower (133138/91375), or should it be interpreted differently?

import Mathlib
set_option autoImplicit false

#count_heartbeats in
example : 1 + 2 = 3 := by rfl
-- Used 71 heartbeats, which is less than the current maximum of 200000.
#count_heartbeats in
example : 1 + 2 = 3 := by aesop
-- Used 111 heartbeats, which is less than the current maximum of 200000.

#count_heartbeats! in
example : 1 + 2 = 3 := by rfl
-- Min: 71 Max: 71 StdDev: 6%
#count_heartbeats! in
example : 1 + 2 = 3 := by aesop
-- Min: 110 Max: 111 StdDev: 6%

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true

example : 1 + 2 = 3 := by rfl
-- [Elab.async] [1033.000000] Lean.addDecl
-- [Elab.async] [71.000000] Lean.compileDecls ▶
-- [Elab.command] [91375.000000] example : 1 + 2 = 3 := by rfl ▶
-- [Elab.async] [54.000000] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask
-- [Elab.async] [8728.000000] Lean.Elab.Command.runLintersAsync ▶
-- [Elab.command] [53.000000]
-- [Elab.async] [5299.000000] Lean.Elab.Command.runLintersAsync ▶
example : 1 + 2 = 3 := by aesop
-- [Elab.async] [1003.000000] Lean.addDecl ▶
-- [Elab.async] [71.000000] Lean.compileDecls ▶
-- [Elab.command] [133138.000000] example : 1 + 2 = 3 := by aesop ▶
-- [Elab.async] [54.000000] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask
-- [Elab.async] [8677.000000] Lean.Elab.Command.runLintersAsync ▶
-- [Elab.command] [53.000000]
-- [Elab.async] [5284.000000] Lean.Elab.Command.runLintersAsync ▶

[Louis Cabarion]

Would it make sense to move this message to the #metaprogramming / tactics channel? Unfortunately, I don’t have permission to do that myself.