maxHeartbeats bound

Stream: lean4

[Yury G. Kudryashov]

Can we ask Lean to report the number of heartbeats used in a lemma? I can do a binary search with set_option maxHeartbeats _ in but I hope that there is a better way.

[Scott Morrison]

I'm sure we can. The relevant function is (← IO.getNumHeartbeats), which returns the number of heartbeats used so far in the current thread. Copying the framework of something like whatsnew in (but much simpler!) would let you run that before and after running the enclosed command of a count_heartbeats in.

[Scott Morrison]

elab "count_heartbeats " "in" ppLine cmd:command : command => do
  let start ← IO.getNumHeartbeats
  try
    elabCommand cmd
  finally
    let finish ← IO.getNumHeartbeats
    logInfo m!"{finish - start}"

count_heartbeats in
def f := 1

[Yury G. Kudryashov]

Thank you!

[Scott Morrison]

Are you doing the PR or am I? :-)

[Yury G. Kudryashov]

You

[Scott Morrison]

The implementation grew slightly: #5365

It now:

• sets maxHeartbeats 0 in the enclosed command
• checks whether or not it exceeds the current limit
• if it does, provides a "Try this:" suggestion of set_option maxHeartbeats 2^k*200000 in, for the least value of k that works.

[Kevin Buzzard]

count_heartbeats has been super-useful for me for benchmarking changes to mathlib files. But is the following expected: on branch kbuzzard-finsupp-module2 the declaration Rep.diagonalHomEquiv_symm_apply in the file RepresentationTheory.GroupCohomology.Resolution, count_heartbeats in is reliably informing me that it's taking over 500000 heartbeats, but set_option maxHeartbeats 400000 reliably works fine. Is this expected, or is there some debugging needed, in which case shall I make a mwe?

[Matthew Ballard]

It doubles on each pass. So 250000 doesn’t work but 500000 does here

[Matthew Ballard]

So it’s expected

[Kevin Buzzard]

It is reporting that it takes 500,000, and telling me that I should hence use 800,000, and my observation is that 400,000 works fine.

[Matthew Ballard]

Oh sorry. Misread. Apologies

[Scott Morrison]

That is not as expected!

[Kevin Buzzard]

Ok let me try and reproduce on master

[Kevin Buzzard]

Here's something which works on master:

import Mathlib.RepresentationTheory.GroupCohomology.Resolution

noncomputable section

universe u

variable {k G : Type u} [CommRing k] {n : ℕ}

open CategoryTheory

variable [Group G] {A : Rep k G}

namespace Rep

open GroupCohomology.Resolution

-- set_option maxHeartbeats 400000 in -- works fine
count_heartbeats in
/-
Used 505130 heartbeats, which is greater than the current maximum of 200000.

Try this: set_option maxHeartbeats 800000 in
-/
theorem diagonalHomEquiv_symm_apply' (f : (Fin n → G) → A) (x : Fin (n + 1) → G) :
    ((diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) =
      A.ρ (x 0) (f fun i : Fin n => (x (Fin.castSucc i))⁻¹ * x i.succ) := by
  unfold diagonalHomEquiv
  simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Iso.trans_hom, Iso.refl_inv,
    Category.comp_id, Action.comp_hom, MonoidalClosed.linearHomEquivComm_symm_hom]
  rw [ModuleCat.coe_comp]
  simp only [ModuleCat.coe_comp, Function.comp_apply]
  rw [diagonalSucc_hom_single]
  erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index]
  simp only [one_smul]
  erw [Representation.linHom_apply]
  simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply]
  erw [Finsupp.llift_apply]
  rw [Finsupp.lift_apply]
  erw [Finsupp.sum_single_index]
  rw [one_smul]
  · rw [zero_smul]
  · rw [zero_smul]

I know the proof is horrible, it used to be a big simp block in mathlib3, but that's exactly what I'm actually working on :-)

[Kevin Buzzard]

There's some noise with actual maxHeartbeats but 400000 reliably works fine on this declaration.

[Kevin Buzzard]

The actual reason I care a little about this is that when trying to make speedup PRs one test is "if I now take a declaration that has set_option maxHeartbeats 2^n*default, does my change enable me to reduce it to 2^(n-1)*default?". And this behaviour of count_heartbeats means that you might get false positives. Right now I'm mitigating against this by just changing the defaults on master to get a definitive answer as to whether a change has an effect. But to be honest there have been a bunch of changes recently that could affect heartbeats across mathlib, so it could well be the case that there are a bunch of files now in mathlib master with too-high (or possibly even unnecessary) maxHeartbeats anyway, so this is not something I'm too bothered about; I thought it was worth reporting though.

[Scott Morrison]

I think the "problem" is that some things, notably typeclass synthesis, happen inside a withCurrHeartbeats call (which essentially means: inside this block use the current maxHeartbeats, but start counting from now). This effectively gives them an extension.

(This withCurrHeartbeats call has been there since Leo put in a maxHeartbeats option.)

Thus I suspect count_heartbeats is correctly reporting the total elapsed heartbeats, but nevertheless nothing is being cut off even with a lower maxHeartbeats.

If we want to do something, I'd probably start by seeing what breaks if you just remove the withCurrHeartbeats in SynthInstance.main.