diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean index 969f30cf18a5..aff979c71757 100644 --- a/src/Lean/Linter.lean +++ b/src/Lean/Linter.lean @@ -9,6 +9,7 @@ prelude public import Lean.Linter.Util public import Lean.Linter.Builtin public import Lean.Linter.ConstructorAsVariable +public import Lean.Linter.DefProp public import Lean.Linter.Deprecated public import Lean.Linter.DocsOnAlt public import Lean.Linter.UnusedVariables diff --git a/src/Lean/Linter/DefProp.lean b/src/Lean/Linter/DefProp.lean new file mode 100644 index 000000000000..f0ddfe0f976b --- /dev/null +++ b/src/Lean/Linter/DefProp.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Różowski + +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner +-/ +module + +prelude +public import Lean.Linter.Basic +public import Lean.Linter.Util + +public section + +namespace Lean.Linter +open Elab Command Meta Term + +/-- +Enables the `defProp` linter, which warns when a `def` is used to introduce a +declaration whose type is a `Prop`. Such a declaration should be written using +`theorem` instead. +-/ +register_builtin_option linter.defProp : Bool := { + defValue := false + descr := "enable the `defProp` linter, which warns when a `def` is used to introduce \ + a declaration whose type is a `Prop`; such a declaration should be written using \ + `theorem` instead." +} + +namespace DefProp + +@[inherit_doc linter.defProp] +def defPropLinter : Linter where run := withSetOptionIn fun _ => do + unless getLinterValue linter.defProp (← getLinterOptions) do + return + if (← get).messages.hasErrors then + return + let env ← getEnv + for t in ← getInfoTrees do + for declName in getDeclsByBody t do + let some info := env.find? declName | continue + unless info.isDefinition do continue + let isPropType ← liftTermElabM <| isProp info.type + if isPropType then + logLintIf linter.defProp (← getRef) m!"\ + Definition `{.ofConstName declName}` is a proposition; use `theorem` instead of `def`" + +builtin_initialize addLinter defPropLinter + +end DefProp +end Lean.Linter diff --git a/src/Lean/Linter/EnvLinter/Builtin.lean b/src/Lean/Linter/EnvLinter/Builtin.lean index 565599d44900..9d66145e844a 100644 --- a/src/Lean/Linter/EnvLinter/Builtin.lean +++ b/src/Lean/Linter/EnvLinter/Builtin.lean @@ -25,18 +25,6 @@ public meta section namespace Lean.Linter.EnvLinter -/-- A linter for checking whether the correct declaration constructor (`def` or `theorem`) -has been used. A `def` whose type is a `Prop` should be a `theorem`, and vice versa. -/ -@[builtin_env_linter] def defLemma : EnvLinter where - noErrorsFound := "All declarations correctly marked as def/lemma." - errorsFound := "INCORRECT DEF/LEMMA:" - test declName := do - if ← isAutoDecl declName then return none - let info ← getConstInfo declName - if info.isDefinition then - if ← isProp info.type then return some "is a def, should be a lemma/theorem" - return none - /-- `univParamsGrouped e nm₀` computes for each `Level` occurring in `e` the set of level parameters that appear in it, returning the collection of such parameter sets. diff --git a/src/Lean/Linter/Extra/UnusedDecidableInType.lean b/src/Lean/Linter/Extra/UnusedDecidableInType.lean index bba0cbdd9058..008a581a03b7 100644 --- a/src/Lean/Linter/Extra/UnusedDecidableInType.lean +++ b/src/Lean/Linter/Extra/UnusedDecidableInType.lean @@ -15,6 +15,7 @@ public import Lean.Meta.ForEachExpr public import Lean.Meta.Sorry public import Lean.PrivateName public import Lean.Server.InfoUtils +public import Lean.Linter.Util public section @@ -253,18 +254,6 @@ private def onUnusedInstancesWhere (decl : ConstantVal) (p : Expr → Bool) } logOnUnused unusedParams -/-- Get the `parentDecl`s of every elaborated body in the infotree. -/ -private def getDeclsByBody (t : InfoTree) : List Name := - t.collectNodesBottomUp fun ctx i _ decls => - match i with - | .ofCustomInfo i => - if i.value.typeName == ``Lean.Elab.Term.BodyInfo then - if let some decl := ctx.parentDecl? then - decl :: decls - else decls - else decls - | _ => decls - /-- Get the declarations elaborated in the infotree `t` which are theorems according to the environment. This includes e.g. `instance`s of `Prop` classes in addition to declarations declared diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index 509c5cdd56aa..5747c492eaa3 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Server.InfoUtils public import Lean.Linter.Init +public import Lean.Elab.Term public section @@ -44,3 +45,15 @@ where return some [] else return none) + +/-- Get the `parentDecl`s of every elaborated body in the infotree. -/ +def getDeclsByBody (t : InfoTree) : List Name := + t.collectNodesBottomUp fun ctx i _ decls => + match i with + | .ofCustomInfo i => + if i.value.typeName == ``Lean.Elab.Term.BodyInfo then + if let some decl := ctx.parentDecl? then + decl :: decls + else decls + else decls + | _ => decls diff --git a/tests/elab/env_linter.lean b/tests/elab/env_linter.lean index 4bd6b361e890..a87e6e548ceb 100644 --- a/tests/elab/env_linter.lean +++ b/tests/elab/env_linter.lean @@ -131,7 +131,7 @@ def testGetChecksDefault : CoreM (Array Name) := do return checks.map (·.name) -- dummyBadName and checkUnivs are default, dummyExtraLinter is not -/-- info: #[`checkUnivs, `defLemma, `dummyBadName] -/ +/-- info: #[`checkUnivs, `dummyBadName] -/ #guard_msgs in #eval testGetChecksDefault @@ -140,7 +140,7 @@ def testGetChecksExtra : CoreM (Array Name) := do let checks ← getChecks (scope := .extra) (runOnly := none) return checks.map (·.name) -/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/ +/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/ #guard_msgs in #eval testGetChecksExtra @@ -149,7 +149,7 @@ def testGetChecksAll : CoreM (Array Name) := do let checks ← getChecks (scope := .all) (runOnly := none) return checks.map (·.name) -/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/ +/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/ #guard_msgs in #eval testGetChecksAll @@ -181,7 +181,7 @@ def testLintCore : CoreM (Array (Name × Nat)) := do let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters return results.map fun (linter, msgs) => (linter.name, msgs.size) -/-- info: #[(`checkUnivs, 0), (`defLemma, 0), (`dummyBadName, 1)] -/ +/-- info: #[(`checkUnivs, 0), (`dummyBadName, 1)] -/ #guard_msgs in #eval testLintCore @@ -210,7 +210,7 @@ def testFormatResults : CoreM Format := do return (← msg.format) /-- -info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 3 linters +info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 2 linters /- The `dummyBadName` linter reports: found bad names -/ @@ -229,7 +229,7 @@ def testFormatResultsClean : CoreM Format := do return (← msg.format) /-- -info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 3 linters +info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 2 linters -/ #guard_msgs in #eval testFormatResultsClean diff --git a/tests/lake/tests/builtin-lint/ExtraViolations.lean b/tests/lake/tests/builtin-lint/ExtraViolations.lean index c6c0c410fd0d..e4e00ea3231a 100644 --- a/tests/lake/tests/builtin-lint/ExtraViolations.lean +++ b/tests/lake/tests/builtin-lint/ExtraViolations.lean @@ -1,5 +1,9 @@ import Linters +-- `linter.defProp` is off by default for bootstrapping reasons; enable it +-- here so `shouldBeTheoremUnderExtra` still fires when default linters run. +set_option linter.defProp true + -- This name ends with 'Extra' — the dummyExtra linter should flag it. def badNameExtra : Nat := 1 @@ -13,7 +17,7 @@ example : True := by -- the builtin extra `dupNamespace` text linter should flag it. def Dup.Dup.violation : Nat := 2 --- This uses `def` for a Prop — the default `defLemma` linter should flag this +-- This uses `def` for a Prop — the default `defProp` linter should flag this -- whenever default linters run, including under `--extra`. def shouldBeTheoremUnderExtra : 1 = 1 := rfl diff --git a/tests/lake/tests/builtin-lint/Main.lean b/tests/lake/tests/builtin-lint/Main.lean index dab87ea09fc3..1eb086623e18 100644 --- a/tests/lake/tests/builtin-lint/Main.lean +++ b/tests/lake/tests/builtin-lint/Main.lean @@ -1,14 +1,18 @@ import Main.Sub --- This uses `def` for a Prop — the `defLemma` linter should flag this. +-- `linter.defProp` is off by default for bootstrapping reasons; enable it +-- here so the test scenarios that exercise default lint mode still trigger it. +set_option linter.defProp true + +-- This uses `def` for a Prop — the `defProp` linter should flag this. def shouldBeTheorem : 1 = 1 := rfl --- This is annotated to be skipped by `defLemma` — no import needed. -@[builtin_nolint defLemma] +-- `set_option` disables `defProp` locally so this violation is not flagged. +set_option linter.defProp false in def skippedViolation : 2 = 2 := rfl -- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`, --- so `defLemma` should flag it. +-- so `defProp` should flag it. @[reducible, instance] def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩ diff --git a/tests/lake/tests/builtin-lint/Main/Sub.lean b/tests/lake/tests/builtin-lint/Main/Sub.lean index dfe131b8b032..56206a92d722 100644 --- a/tests/lake/tests/builtin-lint/Main/Sub.lean +++ b/tests/lake/tests/builtin-lint/Main/Sub.lean @@ -1,5 +1,9 @@ --- Env-linter violation: `def` on a Prop — should be caught by `defLemma` --- regardless of build-time options, since env linters run post-build. +-- `linter.defProp` is off by default for bootstrapping reasons; enable it +-- here so this transitive-import test still captures the violation in the +-- module's lint log. +set_option linter.defProp true + +-- `def` on a Prop — caught by the `defProp` linter at build time. def shouldBeTheoremInSub : 1 = 1 := rfl -- Default text-linter violation: `linter.unusedVariables` has `defValue := true`, diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh index edbb83fd7880..98ab53af650e 100755 --- a/tests/lake/tests/builtin-lint/test.sh +++ b/tests/lake/tests/builtin-lint/test.sh @@ -30,10 +30,10 @@ lake_out lint --lint-only unusedVariables TextLints || true match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out no_match_pat 'missing doc string' produced.out -# --builtin-lint should detect the defLemma violation in Main (the default target) +# --builtin-lint should detect the defProp violation in Main (the default target) lake_out lint --builtin-lint || true match_pat 'shouldBeTheorem' produced.out -match_pat 'is a def, should be a lemma/theorem' produced.out +match_pat 'is a proposition; use `theorem` instead of `def`' produced.out # `@[reducible, instance]` on a `def` of Prop type keeps it a `def`, so flag it. match_pat 'reducibleInstShouldBeTheorem' produced.out # Plain `instance` of Prop type is elaborated as a theorem; it should not be flagged. @@ -45,8 +45,8 @@ match_pat 'only occur together' produced.out # builtin_nolint checkUnivs should suppress the warning no_match_pat 'badUnivSkipped' produced.out -# --lint-only defLemma should run only the defLemma linter -lake_out lint --lint-only defLemma || true +# --lint-only defProp should run only the defProp linter +lake_out lint --lint-only defProp || true match_pat 'shouldBeTheorem' produced.out no_match_pat 'badUnivDecl' produced.out @@ -57,8 +57,9 @@ no_match_pat 'badUnivDecl' produced.out # package, so passing any module of a package flips the flag for every module # in that package. -# Env linters run post-build against `importModules`-loaded decls, so -# `defLemma` catches `shouldBeTheoremInSub` regardless of override scope. +# `defProp` runs during the build of each module, so its warning for +# `shouldBeTheoremInSub` is captured in `Main.Sub`'s lint log and re-emitted +# via `collectTextLints` when `Main` is linted. lake_out lint --builtin-lint Main || true match_pat 'shouldBeTheoremInSub' produced.out @@ -81,7 +82,7 @@ test_run lint --builtin-only Clean # Without --extra, the extra linters (both the env linter and the dummy extra # text linter in Linters.lean) must not run. Default linters still do, so the -# `defLemma` violation in this file fires. +# default `defProp` linter's violation in this file fires. lake_out lint --builtin-only ExtraViolations || true no_match_pat 'badNameExtra' produced.out no_match_pat 'extra text linter saw a declaration' produced.out @@ -91,7 +92,7 @@ no_match_pat 'tac1 <;> tac2' produced.out no_match_pat 'Dup.Dup.violation' produced.out # Builtin extra text linter `unreachableTactic` is non-default, so silent. no_match_pat 'this tactic is never executed' produced.out -# Default env linter `defLemma` runs and flags the def-of-Prop in this file. +# Default `defProp` linter runs and flags the def-of-Prop in this file. match_pat 'shouldBeTheoremUnderExtra' produced.out # --extra should run default linters together with the non-default (extra) @@ -109,7 +110,7 @@ match_pat 'Dup.Dup.violation' produced.out match_pat "namespace .*Dup.* is duplicated" produced.out # Builtin `unreachableTactic` extra text linter fires under --extra. match_pat 'this tactic is never executed' produced.out -# --extra also runs default linters, so `defLemma` flags this file's violation. +# --extra also runs default linters, so `defProp` flags this file's violation. match_pat 'shouldBeTheoremUnderExtra' produced.out # --extra on TextLints: default `linter.unusedVariables` fires (default @@ -141,15 +142,15 @@ no_match_pat 'badNameExtra' produced.out no_match_pat 'shouldBeTheorem' produced.out # Multiple --lint-only flags accumulate: both named linters should run -lake_out lint --lint-only defLemma --lint-only checkUnivs || true +lake_out lint --lint-only defProp --lint-only checkUnivs || true match_pat 'shouldBeTheorem' produced.out match_pat 'badUnivDecl' produced.out no_match_pat 'badNameExtra' produced.out # Last-wins: --extra overrides a prior --lint-all and clears --lint-only. -# Since --extra runs both default and extra linters, the default `defLemma` +# Since --extra runs both default and extra linters, the default `defProp` # violation in ExtraViolations.lean fires too. -lake_out lint --lint-all --lint-only defLemma --extra || true +lake_out lint --lint-all --lint-only defProp --extra || true match_pat 'badNameExtra' produced.out match_pat 'shouldBeTheoremUnderExtra' produced.out @@ -160,13 +161,13 @@ match_pat 'badNameExtra' produced.out match_pat 'shouldBeTheorem' produced.out # Last-wins: --extra clears a previously accumulated --lint-only. Default -# linters still run under --extra, so `defLemma` fires on its file's violation. -lake_out lint --lint-only defLemma --extra || true +# linters still run under --extra, so `defProp` fires on its file's violation. +lake_out lint --lint-only defProp --extra || true match_pat 'badNameExtra' produced.out match_pat 'shouldBeTheoremUnderExtra' produced.out # --lint-only after --extra: the named linter runs (selection ignores scope) -lake_out lint --extra --lint-only defLemma || true +lake_out lint --extra --lint-only defProp || true match_pat 'shouldBeTheorem' produced.out no_match_pat 'badNameExtra' produced.out @@ -193,7 +194,7 @@ lake_out lint --extra ExtraViolations || true match_pat 'badNameExtra' produced.out # --lint-only implicitly enables builtin lint -lake_out lint --lint-only defLemma || true +lake_out lint --lint-only defProp || true match_pat 'shouldBeTheorem' produced.out # builtinLint = false: check-lint fails (no lint driver and builtin linting disabled)