Comments from Original PR #21182

This section contains 6 comment(s) from the original PR, excluding bot comments.

@mathlib-bors (2025-01-28 19:03 UTC):
✌️ joneugster can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@adomani (2025-01-28 19:09 UTC):
Sorry about the change of heart: I tried it out on the "obvious" file and it throws many more exceptions than I would like.

It is still an improvement over the previous version, but not yet good to go!

bors d-

@adomani (2025-01-28 19:12 UTC):
(By the way, bors d- probably does nothing. Out of curiousity, I'll try a different bors command, not because I think that you will merge this as is, but to see if it works!

bors delegate=[]
)

@adomani (2025-01-28 19:14 UTC):
Oh well, a failed experiment. 🤷

@adomani (2025-01-28 19:17 UTC):
So, since it has come down to finding which hack is most successful, one approach that I would try is to "extend" the first declId that the syntax contains with an extra string. Effectively, trying to elaborate theorem A.B.C ... as theorem A.B.Ccount_heartbeats_linter ....

This is still not very robust, but, because it is not messing with the namespace, it may fail less often. Recursive calls will likely still not work, and use the declaration that has just been added to the environment, as will declarations that contain declIds before the actual declId of the declaration, but... nobody's perfect!

@joneugster (2026-02-15 03:30 UTC):
Returning to this, I'm not fully aware of all the discussion linked at #23905 but it looks like the current implementation of #count_heartbeats is broken on master and it seems to work with this fix, so I'm putting this back on the queue.

(If there is a better re-implementation of the command, I'd be happy to review that and close this fix once a reimplementation has been merged.)

🔒 Permission denied

Existing reviewers: click here to make joneugster a reviewer

PR summary 88bb6d226a

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary