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

[Michael Stoll]

It seems that #count_heartbeats in is currently broken:

import Mathlib.NumberTheory.NumberField.FinitePlaces

namespace IsDedekindDomain.HeightOneSpectrum
variable {K : Type*} [Field K] [NumberField K]
open NumberField.FinitePlace NumberField.RingOfIntegers
  NumberField.RingOfIntegers.HeightOneSpectrum
open scoped NumberField

set_option profiler true
set_option profiler.threshold 10

/-
tactic execution of Mathlib.Tactic.convert took 3.5s
type checking took 4.3s
-/
lemma foo₁ (v : HeightOneSpectrum (𝓞 K)) (x : K) :
    (equivHeightOneSpectrum.symm v) x = ‖embedding v x‖ := by
  have : v = (equivHeightOneSpectrum.symm v).maximalIdeal := by
    change v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)
    exact (Equiv.apply_symm_apply _ v).symm
  convert (norm_embedding_eq (equivHeightOneSpectrum.symm v) x).symm

set_option profiler false

#count_heartbeats in -- Used 336 heartbeats
lemma foo₂ (v : HeightOneSpectrum (𝓞 K)) (x : K) :
    (equivHeightOneSpectrum.symm v) x = ‖embedding v x‖ := by
  have : v = (equivHeightOneSpectrum.symm v).maximalIdeal := by -- this tactic is never executed
    change v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)
    exact (Equiv.apply_symm_apply _ v).symm
  -- 'convert (norm_embedding_eq (equivHeightOneSpectrum.symm v) x).symm' tactic does nothing
  -- this tactic is never executed
  convert (norm_embedding_eq (equivHeightOneSpectrum.symm v) x).symm

(This is an example that came up in #28567.)

The profiler output shows that the declaration is rather slow, but #count_heartbeats in gives a rather small number and also has the effect of the "unused tactic" linter triggering on two of the tactic invocations.
If the effect really is that these tacticts do nothing, then this explains the small heartbeat count :smile:, but it makes #count_heartbeats in rather unusable.

[Michael Stoll]

Might this be some kind of side-effect of parallelism?

[Damiano Testa]

Does it give more realistic results with set_option Elab.async false in?

Several linters have been affected by parallelism.

[Michael Stoll]

Damiano Testa said:

Does it give more realistic results with set_option Elab.async false in?

Several linters have been affected by parallelism.

Yes:

set_option Elab.async false in
#count_heartbeats in -- Used 126266 heartbeats
lemma foo₂ (v : HeightOneSpectrum (𝓞 K)) (x : K) :
    (equivHeightOneSpectrum.symm v) x = ‖embedding v x‖ := by
  have : v = (equivHeightOneSpectrum.symm v).maximalIdeal := by
    change v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)
    exact (Equiv.apply_symm_apply _ v).symm
  convert (norm_embedding_eq (equivHeightOneSpectrum.symm v) x).symm

and no linter warnings.

Should #count_heartbeats do set_option Elab.async false by default?

[Damiano Testa]

Yes, I think so. Unless there is a better way to get the actual timing without crippling parallelism.

[Kevin Buzzard]

Bandaid at #29311 (partly done in an attempt to provoke someone to do the actual fix, which unfortunately I am not competent to do). I am also tempted to open an issue. I sometimes find #count_heartbeats very useful when debugging but often find myself trawling through the Zulip trying to figure out how to make it work.

[Kim Morrison]

fix: add Elab.async false in #count_heartbeats #29335

I have not yet added an effective test. Could someone else please attempt that, either here or in a different PR? I'd prefer not to take that on.

I did verify that it works as expected at docs#FractionIdeal.quotientEquiv.