Skip to content

linter.countHeartbeats is broken #23905

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kbuzzard opened this issue Apr 10, 2025 · 1 comment
Open

linter.countHeartbeats is broken #23905

kbuzzard opened this issue Apr 10, 2025 · 1 comment

Comments

@kbuzzard
Copy link
Member

kbuzzard commented Apr 10, 2025

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.

@kbuzzard
Copy link
Member Author

kbuzzard commented May 7, 2025

Damiano's code here

#mathlib4 > Frustrating debugging problem @ 💬

worked wonders for me on mathlib of a couple of weeks ago. NB you don't use count_heartbeats, you just import the file and it profiles all the declarations.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant