count_heartbeats bug?

Stream: maths

[Johan Commelin]

I took the example from https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Heavy.20rfl/near/469774488 and added count_heartbeats in to the examples.
The result is that I have several threads eating up 100% of about half of my cores. And they don't die down. Not even after a few minutes.
I'm using lean.nvim.

import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

variable (R : Type*) {V V' P P' : Type*}
variable [OrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P]
variable [AddCommGroup V'] [Module R V'] [AddTorsor V' P']

open AffineMap

def Sbtw (x y z : P) : Prop := y ∈ lineMap x y '' Set.Icc (0 : R) 1 ∧ y ≠ x ∧ y ≠ z

variable {R}

theorem Function.Injective.sbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  sorry

-- 146454 heartbeats
count_heartbeats in
lemma slow {x y z : P} (f : P ≃ᵃ[R] P') : Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  let hf : Function.Injective f.toAffineMap := AffineEquiv.injective f
  Function.Injective.sbtw_map_iff hf

-- 762 heartbeats
count_heartbeats in
lemma fast {x y z : P} (f : P ≃ᵃ[R] P') : Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  let hf : Function.Injective f.toAffineMap := AffineEquiv.injective f
  hf.sbtw_map_iff

[Johan Commelin]

Can anyone reproduce?

[Johan Commelin]

I was just messing around in the file a bit. Nothing special.

[Heather Macbeth]

I have experienced this too (in VSCode), although I don't have a precise example to reproduce it. I have switched to a workflow of commenting out count_heartbeats before editing, which seems to avoid this.

[Matthew Ballard]

I have had sporadic cases of this also

[Kim Morrison]

Were you editing the contents of the lemmas wrapped in count_heartbeats? If so, expected behaviour. :-)

[Kim Morrison]

That I don't know how to fix.

[Mario Carneiro]

Can you explain what is happening / how this is implemented?

[Kim Morrison]

From file#Util/CountHeartbeats

elab "count_heartbeats " "in" ppLine cmd:command : command => do
  let start ← IO.getNumHeartbeats
  try
    elabCommand (← `(command| set_option maxHeartbeats 0 in $cmd))
  finally
    let finish ← IO.getNumHeartbeats
    let elapsed := (finish - start) / 1000
    let max := (← Command.liftCoreM getMaxHeartbeats) / 1000
    if elapsed < max then
      logInfo m!"Used {elapsed} heartbeats, which is less than the current maximum of {max}."
    else
      let mut max' := max
      while max' < elapsed do
        max' := 2 * max'
      logInfo m!"Used {elapsed} heartbeats, which is greater than the current maximum of {max}."
      let m : TSyntax `num := quote max'
      Command.liftCoreM <| MetaM.run' do
        Lean.Meta.Tactic.TryThis.addSuggestion (← getRef)
          (← set_option hygiene false in `(command| set_option maxHeartbeats $m in $cmd))

[Mario Carneiro]

what's the issue?

[Mario Carneiro]

is it that the first call runs without a timeout and hence can't be interrupted by the elaborator cancellation signal?

[Floris van Doorn]

I think this is the same as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/count_heartbeats.20CPU.20usage ?

[Kim Morrison]

Yes, I think people are observing that if you type in the command wrapped in count_heartbeats, 100s of non-cancellable copies of the command are spawned.