Skip to content

chore: remove the defLemma linter #1863

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
grunweg wants to merge 2 commits into
base: main
Choose a base branch
from
+7 −37
Open

chore: remove the defLemma linter #1863

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c91007f
chore: remove the defLemma linter
grunweg Jun 19, 2026
b64b257
Fix tests
grunweg Jun 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 2 additions & 29 deletions Batteries/Tactic/Lint/Misc.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,35 +111,8 @@ their value, and allow arguments starting with `_` to be unused. -/
let (none) ← findDocString? (← getEnv) declName | return none
return m!"{kind} missing documentation string"

/-- A linter for checking whether the correct declaration constructor (definition or theorem)
has been used. -/
@[env_linter] def defLemma : Linter where
noErrorsFound := "All declarations correctly marked as def/lemma."
errorsFound := "INCORRECT DEF/LEMMA:"
test declName := do
if (← isAutoDecl declName) || (← isImplicitReducible declName) then
return none
-- leanprover/lean4#2575:
-- projections are generated as `def`s even when they should be `theorem`s
if ← isProjectionFn declName then return none
let info ← getConstInfo declName
let isThm ← match info with
| .defnInfo .. => pure false
| .thmInfo .. => pure true
| _ => return none
match isThm, ← isProp info.type with
| true, false => pure "is a lemma/theorem, should be a def"
| false, true => pure "is a def, should be lemma/theorem"
| _, _ => return none

/-- A linter for checking whether statements of declarations are well-typed.

This linter is disabled by default: declarations are already type-checked when added to the
environment, so re-checking every statement is redundant in normal use. As an alternative
defence-in-depth measure for catching kernel/elaborator bugs, prefer running an external
checker such as `lean4checker` or `trepplein`.
-/
@[env_linter disabled] def checkType : Linter where
/-- A linter for checking whether statements of declarations are well-typed. -/
@[env_linter] def checkType : Linter where
noErrorsFound :=
"The statements of all declarations type-check with default reducibility settings."
errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK."
Expand Down
10 changes: 5 additions & 5 deletions BatteriesTest/lintTrace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,11 @@ trace: [Batteries.Lint] Running linters:

/--
trace: [Batteries.Lint] Running linters:
defLemma
[Batteries.Lint] - defLemma: (0/2) Starting...
[Batteries.Lint] - defLemma: (1/2) Getting...
[Batteries.Lint] - defLemma: (2/2) Passed!
unusedHavesSuffices
[Batteries.Lint] - unusedHavesSuffices: (0/2) Starting...
[Batteries.Lint] - unusedHavesSuffices: (1/2) Getting...
[Batteries.Lint] - unusedHavesSuffices: (2/2) Passed!
[Batteries.Lint] Completed linting!
-/
#guard_msgs in
#lint- only defLemma
#lint- only unusedHavesSuffices
3 changes: 0 additions & 3 deletions BatteriesTest/lint_coinductive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,5 @@ mutual
| mk : ¬tick → tock
end

#guard_msgs in
#lint- only defLemma

#guard_msgs in
#lint- only docBlame
Loading