Skip to content

fix: make grind_lint see custom grind attrs#13839

Open
raphael-solace wants to merge 1 commit into
leanprover:masterfrom
raphael-solace:rc/grind-lint-custom-sets
Open

fix: make grind_lint see custom grind attrs#13839
raphael-solace wants to merge 1 commit into
leanprover:masterfrom
raphael-solace:rc/grind-lint-custom-sets

Conversation

@raphael-solace
Copy link
Copy Markdown

@raphael-solace raphael-solace commented May 25, 2026

This PR makes #grind_lint consider all registered grind attribute extensions instead of only the built-in @[grind] extension.

Custom grind sets created with register_grind_attr can now be skipped, muted, and included by lint checks, which is useful for downstream libraries that maintain specialized automation sets.

Closes #13733.

@raphael-solace
Copy link
Copy Markdown
Author

changelog-tactics

@github-actions github-actions Bot added changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels May 25, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7f13a8988f0018f404d4bb0954f95122b8855084 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-25 13:15:00)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7f13a8988f0018f404d4bb0954f95122b8855084 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-25 13:15:03)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

#grind_lint does not recognize grind sets

2 participants