linter.countHeartbeats seems to be currently broken. There was a discussion about the idea of counting heartbeats for every declaration in a file [here](#mathlib4 > count_heartbeats for all declarations in a file? @ 💬) and this prompted the addition of the linter in #20421 . But it seems to me that currently (v4.19.0-rc2) if you try it on any mathlib file, it just reports that all declarations take exactly the same number of heartbeats. See also #21182 .

To reproduce: open a random file in mathlib (e.g. Mathlib/Algebra/Order/Field/Basic.lean), type set_option linter.countHeartbeats true or #count_heartbeats at the top of the file, and observe that every single declaration in the file is now reported as using the same number of heartbeats.