Skip to content

chore: turn defLemma linter into Lean.Linter and rename it to defProp - #13803

Merged
wkrozowski merged 6 commits into
leanprover:masterfrom
wkrozowski:wojciech/builtinEnvLinter
May 28, 2026
Merged

chore: turn defLemma linter into Lean.Linter and rename it to defProp#13803
wkrozowski merged 6 commits into
leanprover:masterfrom
wkrozowski:wojciech/builtinEnvLinter

Conversation

@wkrozowski

@wkrozowski wkrozowski commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR renames the defLemma linter to defProp and clarifies
its warning message.

The linter is also moved out of the EnvLinter framework into its own file
Lean.Linter.DefProp, since it now processes elaboration info trees per command.
The helper getDeclsByBody is exposed in Lean.Linter.Util for reuse.

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label May 20, 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 20, 2026
@leanprover-bot

leanprover-bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-20 16:55:47)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf38e594f659ddc5f0bea8b3699d8512dbb99220 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-27 17:20:55)

@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 May 20, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 20, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-13803 has successfully built against this PR. (2026-05-20 17:52:51) View Log
  • ✅ Mathlib branch lean-pr-testing-13803 has successfully built against this PR. (2026-05-20 22:18:27) View Log
  • ✅ Mathlib branch lean-pr-testing-13803 has successfully built against this PR. (2026-05-21 00:13:52) View Log
  • ✅ Mathlib branch lean-pr-testing-13803 has successfully built against this PR. (2026-05-25 10:58:58) View Log
  • ✅ Mathlib branch lean-pr-testing-13803 has successfully built against this PR. (2026-05-25 19:03:12) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf38e594f659ddc5f0bea8b3699d8512dbb99220 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-27 17:20:53)

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
2e8c086
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
3f71d34
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
3ac9e7d
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
f4cbf4c
@wkrozowski wkrozowski changed the title chore: turn defLemma linter into Lean.Linter (WIP) chore: turn defLemma linter into Lean.Linter and rename it to defProp (WIP) May 25, 2026
@wkrozowski wkrozowski changed the title chore: turn defLemma linter into Lean.Linter and rename it to defProp (WIP) chore: move and rename defLemma linter to defProp May 25, 2026
@wkrozowski wkrozowski changed the title chore: move and rename defLemma linter to defProp chore: turn defLemma linter into Lean.Linter and rename it to defProp. May 25, 2026
@wkrozowski wkrozowski changed the title chore: turn defLemma linter into Lean.Linter and rename it to defProp. chore: turn defLemma linter into Lean.Linter and rename it to defProp May 25, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
98531c0
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 25, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
94aec3c
@wkrozowski wkrozowski mentioned this pull request May 25, 2026
Merged
@wkrozowski
wkrozowski marked this pull request as ready for review May 25, 2026 16:06
@wkrozowski wkrozowski added the lake-ci Run all Lake tests label May 25, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
e67417b
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 25, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#13803
26fc091
@wkrozowski
wkrozowski added this pull request to the merge queue May 28, 2026
Merged via the queue into leanprover:master with commit 4e59cdf May 28, 2026
18 checks passed
github-merge-queue Bot pushed a commit that referenced this pull request May 28, 2026
@wkrozowski
chore: make checkUnivs linter into Lean.Linter (#13832)
cc503a5 
This PR makes `checkUnivs` linter into `Lean.Linter`.

Stacked on top of #13803.
wkrozowski added a commit to wkrozowski/lean4 that referenced this pull request May 29, 2026
@wkrozowski
chore: turn defLemma linter into Lean.Linter and rename it to `de…
73ff16f 
…fProp` (leanprover#13803)

This PR renames the `defLemma` linter to `defProp` and clarifies
its warning message.

The linter is also moved out of the `EnvLinter` framework into its own
file
`Lean.Linter.DefProp`, since it now processes elaboration info trees per
command.
The helper `getDeclsByBody` is exposed in `Lean.Linter.Util` for reuse.
wkrozowski added a commit to wkrozowski/lean4 that referenced this pull request May 29, 2026
@wkrozowski
chore: make checkUnivs linter into Lean.Linter (leanprover#13832)
723b820 
This PR makes `checkUnivs` linter into `Lean.Linter`.

Stacked on top of leanprover#13803.
@grunweg grunweg mentioned this pull request Jun 19, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms lake-ci Run all Lake tests 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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@wkrozowski @leanprover-bot