Skip to content

feat: report text linter diagnostics by module#13853

Draft
wkrozowski wants to merge 1 commit into
leanprover:masterfrom
wkrozowski:wojciech/reportTextLintersByFile
Draft

feat: report text linter diagnostics by module#13853
wkrozowski wants to merge 1 commit into
leanprover:masterfrom
wkrozowski:wojciech/reportTextLintersByFile

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

This PR makes lake lint --builtin-lint group saved text linter diagnostics by the module
that produced them, rather than printing one combined block under the
top-level module being linted. Each contributing submodule now gets its own
-- Text linter diagnostics in <module>: header, mirroring how the
environment-linter side already groups results.

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label May 26, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 26, 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 55cf1d71e8dc1217c559d6426571d237beb84e46 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-26 16:42:57)

@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 55cf1d71e8dc1217c559d6426571d237beb84e46 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-26 16:42:59)

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

Labels

changelog-language Language features and metaprograms 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.

2 participants