Skip to content

feat: introduce findMatchingDecl? for code quality checks in Lean.Linter - #14880

Merged
wkrozowski merged 4 commits into
leanprover:masterfrom
wkrozowski:wkr/findPosition
Sep 4, 2026
Merged

feat: introduce findMatchingDecl? for code quality checks in Lean.Linter#14880
wkrozowski merged 4 commits into
leanprover:masterfrom
wkrozowski:wkr/findPosition

Conversation

@wkrozowski

@wkrozowski wkrozowski commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

This PR adds Lean.Linter.findMatchingDecl?, which finds the declaration a piece of syntax belongs to by searching the current command's info trees for declarations whose declaration range contains it, together with Lean.Linter.findCodeQualitySource? and Lean.Linter.findCodeQualitySource, which turn that declaration into a code-quality Source (the latter falling back to the current module when no declaration matches). This gives linters a way to attribute diagnostics and code-quality entries to the declaration being elaborated.

The helpers are exercised by a new package test, tests/pkg/find_matching_decl, which registers a linter reporting the matched declaration and derived source for each command. It covers plain definitions, inductives, mutual blocks, classes, instances, and commands with no associated declaration.

@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 Aug 21, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 21, 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 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 14:14:39)
  • 💥 Mathlib branch lean-pr-testing-14880 build failed against this PR. (2026-09-03 10:13:48) View Log
  • 💥 Mathlib branch lean-pr-testing-14880 build failed against this PR. (2026-09-03 11:18:16) View Log
  • 💥 Mathlib branch lean-pr-testing-14880 build failed against this PR. (2026-09-03 13:00:11) View Log
  • 💥 Mathlib branch lean-pr-testing-14880 build failed against this PR. (2026-09-03 13:08:56) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-09-03 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-03 13:22:35)

@leanprover-bot

leanprover-bot commented Aug 21, 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 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 14:14:40)
  • ✅ Reference manual branch lean-pr-testing-14880 has successfully built against this PR. (2026-09-03 10:13:32) View Log
  • 🟡 Reference manual branch lean-pr-testing-14880 build against this PR didn't complete normally. (2026-09-03 10:14:34) View Log
  • ✅ Reference manual branch lean-pr-testing-14880 has successfully built against this PR. (2026-09-03 11:10:30) View Log
  • 🟡 Reference manual branch lean-pr-testing-14880 build against this PR didn't complete normally. (2026-09-03 11:12:32) View Log
  • ✅ Reference manual branch lean-pr-testing-14880 has successfully built against this PR. (2026-09-03 12:52:14) View Log
  • 🟡 Reference manual branch lean-pr-testing-14880 build against this PR didn't complete normally. (2026-09-03 12:54:56) View Log
  • ✅ Reference manual branch lean-pr-testing-14880 has successfully built against this PR. (2026-09-03 13:03:36) View Log
  • 🟡 Reference manual branch lean-pr-testing-14880 build against this PR didn't complete normally. (2026-09-03 13:03:46) View Log
  • ✅ Reference manual branch lean-pr-testing-14880 has successfully built against this PR. (2026-09-03 13:28:23) View Log
  • 🟡 Reference manual branch lean-pr-testing-14880 build against this PR didn't complete normally. (2026-09-03 13:29:35) View Log

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Sep 3, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 3, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
@wkrozowski wkrozowski added the changelog-no Do not include this PR in the release changelog label Sep 3, 2026
@wkrozowski wkrozowski changed the title feat: introduce findMatchingDecl? for code quality checks wrapped in Lean.Linter (DRAFT) feat: introduce findMatchingDecl? for code quality checks in Lean.Linter Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
@wkrozowski
wkrozowski marked this pull request as ready for review September 3, 2026 13:52
@wkrozowski
wkrozowski added this pull request to the merge queue Sep 4, 2026
Merged via the queue into leanprover:master with commit 67526ae Sep 4, 2026
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-no Do not include this PR in the release changelog mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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