Is count_heartbeats broken

Stream: mathlib4

[Yury G. Kudryashov]

I have an impression that #count_heartbeats in is broken on master, probably because Lean now elaborates theorems in threads. I don't have a #mwe at the moment, but

• replacing aesop with a term proof didn't change the reported number;
• when I add #count_heartbeats to some definitions, the "unused arguments" linter starts complaining sometimes.

[Kevin Buzzard]

#count_heartbeats is definitely broken #23905, as it says in your title, but in your question you're asking about #count_heartbeats in.

[Yury G. Kudryashov]

I think that the function used by both of them is broken.

[Kevin Buzzard]

import Mathlib

#count_heartbeats in -- 71
example : 2 + 2 = 4 := by
  rfl

#count_heartbeats in -- 108
example : 2 + 2 = 4 := by
  aesop

#count_heartbeats in -- 81
example : 2 + 2 = 4 := by
  tauto

I can't reproduce what you're seeing (I used #count_heartbeats in a lot over the weekend)

[Yury G. Kudryashov]

I had a term mode proof with by _ here and there. Sorry, I'm going to bed now. I'll try to make a #mwe tomorrow