Skip to content

feat: lake: add code quality mode to lake lint - #14622

Merged
wkrozowski merged 14 commits into
leanprover:masterfrom
wkrozowski:wkr/code_quality_run
Aug 6, 2026
Merged

feat: lake: add code quality mode to lake lint#14622
wkrozowski merged 14 commits into
leanprover:masterfrom
wkrozowski:wkr/code_quality_run

Conversation

@wkrozowski

@wkrozowski wkrozowski commented Jul 31, 2026

Copy link
Copy Markdown
Contributor

This PR adds a --code-quality option to lake lint that emits builtin linter results as machine-readable JSON entries instead of human-readable diagnostics. Text-linter warnings are aggregated per module and linter into one entry holding the warning count, and environment-linter findings are reported per flagged declaration; both are keyed by the linter's option name. The option implies --builtin-lint and --builtin-only.

@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 Jul 31, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 31, 2026

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 17dbc815cf3055e73a9e37d854b8427dc1e9c46c --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-31 15:17:58)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42a1d764b58761bdda1a175625d4e9dd8e998d9a --onto f2bcf2e8660ab2d16cf3cb50c8e127de0439a337. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-05 11:24:52)

@leanprover-bot

leanprover-bot commented Jul 31, 2026

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 17dbc815cf3055e73a9e37d854b8427dc1e9c46c --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-31 15:17:59)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 42a1d764b58761bdda1a175625d4e9dd8e998d9a --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-05 11:24:53)

@wkrozowski wkrozowski changed the title feat: add code-quality mode to lake lint (work in progress) feat: add a code quality mode to lake lint Aug 5, 2026
@wkrozowski wkrozowski changed the title feat: add a code quality mode to lake lint feat: lake: add code quality mode to lake lint Aug 5, 2026
@wkrozowski
wkrozowski marked this pull request as ready for review August 5, 2026 14:53
@wkrozowski
wkrozowski requested a review from tydeu as a code owner August 5, 2026 14:53
@wkrozowski
wkrozowski added this pull request to the merge queue Aug 6, 2026
Merged via the queue into leanprover:master with commit 4a37393 Aug 6, 2026
28 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake 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