Skip to content

fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace#21182

Closed
joneugster wants to merge 11 commits intomasterfrom
eugster/count_heartbeats_fix
Closed

fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace#21182
joneugster wants to merge 11 commits intomasterfrom
eugster/count_heartbeats_fix

Conversation

@joneugster
Copy link
Copy Markdown
Contributor

@joneugster joneugster commented Jan 28, 2025 •
edited
Loading

Currently the #count_heartbeat linter reported the heartbeats until it concluded error: [declaration] has already been declared instead of re-elaborating the declaration.

Zulip report

Open in Gitpod

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 28, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 28, 2025 •
edited
Loading

PR summary 88bb6d226a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ MyNamespace.dependent
+ MyNamespace.helper
+ XX
+ XX₂
+ YX'₂
+ a
+ b

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-meta Tactics, attributes or user commands label Jan 28, 2025
joneugster
joneugster commented Jan 28, 2025
View reviewed changes
adomani
adomani reviewed Jan 28, 2025
View reviewed changes
adomani
adomani reviewed Jan 28, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@adomani adomani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me and certainly an improvement over the previous version: thanks!

I am happy to merge this.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 28, 2025

✌️ 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.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 28, 2025
@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jan 28, 2025

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 adomani removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 28, 2025
@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jan 28, 2025

(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=[]
)

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 28, 2025
@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jan 28, 2025

Oh well, a failed experiment. 🤷

@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jan 28, 2025 •
edited
Loading

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 joneugster removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 28, 2025
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 28, 2025
adomani
adomani reviewed Jan 29, 2025
View reviewed changes
adomani
adomani reviewed Jan 29, 2025
View reviewed changes
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2025
@kbuzzard kbuzzard mentioned this pull request Apr 10, 2025
Open
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jun 3, 2025

This pull request has conflicts, please merge master and resolve them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 3, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 15, 2026
@joneugster
Copy link
Copy Markdown
Contributor Author

joneugster commented Feb 15, 2026 •
edited
Loading

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.)

@joneugster joneugster mentioned this pull request Feb 16, 2026
Open
@joneugster
Copy link
Copy Markdown
Contributor Author

joneugster commented Feb 16, 2026

This PR has been migrated to a fork-based workflow: #35413

@joneugster joneugster closed this Feb 16, 2026
@YaelDillies YaelDillies deleted the eugster/count_heartbeats_fix branch March 29, 2026 12:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@adomani adomani adomani left review comments

Assignees

@adomani adomani

Labels

migrated-to-fork t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joneugster @adomani @leanprover-community-bot-assistant