diagnostic tool request

Stream: general

[Johan Commelin]

I am trying to create a MWE of a very slow declaration on bump/v4.12.0.
At the moment I have

-- a very slow version, to check that the decl still compiles, after minimization attempts
set_option maxHeartbeats 800000 in
instance functorCategoryLinear : Linear R (C ⥤ D) where
  <snip>


-- another very slow version, to check that the decl is still slow, after minimization attempts
/--
error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
---
error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
instance functorCategoryLinear' : Linear R (C ⥤ D) where
  <snip>

I would really like to have a command (a version of count_heartbeats in?) that would combine these two:

• check that the decl doesn't have errors
• check that it uses at least x heartbeats.

[Kim Morrison]

Mathlib.Util.Counthearbeats has the components to put this together quickly, I think.

[Kim Morrison]

e.g.

/--
Run a command, optionally restoring the original state, and report just the number of heartbeats.
-/
def elabForHeartbeats (cmd : TSyntax `command) (revert : Bool := true) : CommandElabM Nat := do