feat: lake: add support for running environment linters (#13431)

This PR adds builtin environment linting support to Lake, accessible via
`lake lint` flags. It also introduces two builtin linters upstreamed
from Mathlib (`defLemma` and `checkUnivs`) and a `builtinLint` package
configuration option.

Builtin linting is triggered via flags on `lake lint`:
- `--builtin-lint`: run default builtin linters (in addition to the lint
driver if configured)
- `--builtin-only`: run only builtin linters, skip the lint driver
- `--clippy`: run only non-default (clippy) linters
- `--lint-all`: run all builtin linters (default + clippy)
- `--lint-only <name>`: run a specific builtin linter by name
- Using `--clippy`, `--lint-all`, or `--lint-only` implicitly enables
builtin lint mode

The `builtinLint` package option is a tristate (`Option Bool`):
- `true`: always run builtin lints via `lake lint`; when a lint driver
is also configured, builtin lints run first, then the driver, and the
command fails if either reports errors.
- `false`: never run builtin lints automatically; `lake check-lint`
fails unless a lint driver is configured.
- `none` (default): currently equivalent to `false`; in a future
release, `none` will fall back to builtin lints when no lint driver is
configured.

The linter framework introduces a `LintScope` enum (`.default`,
`.clippy`, `.all`) replacing the previous boolean `clippy` parameter in
`getChecks` and `formatLinterResults`. A `@[builtin_nolint]` attribute
(available without imports) allows suppressing specific linters per
declaration.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

CMakeLists.txt

@@ -86,7 +86,7 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       set(LEANTAR_TARGET x86_64-pc-windows-msvc)
     else()
       set(LEANTAR_ARCHIVE_SUFFIX .tar.gz)
-      if(CMAKE_SYSTEM_PROCESSOR MATCHES "arm64")
+      if(CMAKE_SYSTEM_PROCESSOR MATCHES "arm64|aarch64")
         set(LEANTAR_TARGET_ARCH aarch64)
       else()
         set(LEANTAR_TARGET_ARCH x86_64)

src/Init.lean

@@ -48,3 +48,4 @@ public import Init.BinderNameHint
 public import Init.Task
 public import Init.MethodSpecsSimp
 public import Init.LawfulBEqTactics
+public import Init.Linter

src/Init/Linter.lean

@@ -0,0 +1,15 @@
+/-
+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
+-/
+module
+
+prelude
+public import Init.Notation
+
+public section
+
+/-- `@[builtin_nolint linterName*]` omits the tagged declaration from being checked by
+the named builtin linters in `lake builtin-lint`. -/
+syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr

src/Lean/Elab/BuiltinDo/Match.lean

@@ -203,7 +203,8 @@ private def compileMatch (discrs : Array Term.Discr) (matchType : Expr) (lhss :
 
 private def elabDoMatchCore (discrs : TSyntaxArray ``matchDiscr) (alts : Array DoMatchAltView)
     (nondupDec : DoElemCont) : DoElabM Expr := do
-  let info ← alts.foldlM (fun info alt => info.alternative <$> inferControlInfoSeq alt.rhs) ControlInfo.pure
+  let info ← alts.foldlM (fun info alt => info.alternative <$> inferControlInfoSeq alt.rhs)
+    ControlInfo.empty
   nondupDec.withDuplicableCont info fun dec => do
   trace[Elab.do.match] "discrs: {discrs}, nondupDec.resultType: {nondupDec.resultType}, may postpone: {(← readThe Term.Context).mayPostpone}"
   tryPostponeIfDiscrTypeIsMVar discrs

src/Lean/Elab/DeclModifiers.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.DocString.Add
 public import Lean.Linter.Basic
+import Lean.Linter.EnvLinter.Nolint
 meta import Lean.Parser.Command
 
 public section

src/Lean/Elab/Do/Basic.lean

@@ -587,7 +587,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x newX
-    withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
+    withDeadCode (if callerInfo.noFallthrough then .deadSemantically else .alive) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do

src/Lean/Elab/Do/Control.lean

@@ -232,9 +232,8 @@ def ControlLifter.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM Contr
     breakBase?,
     continueBase?,
     pureBase := controlStack,
-    -- The success continuation `origCont` is dead code iff the `ControlInfo` says that there is no
-    -- regular exit.
-    pureDeadCode := if info.numRegularExits > 0 then .alive else .deadSemantically,
+    -- The success continuation `origCont` is dead code iff the `ControlInfo` says so semantically.
+    pureDeadCode := if info.noFallthrough then .deadSemantically else .alive,
     liftedDoBlockResultType := (← controlStack.stM dec.resultType),
   }
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -16,48 +16,81 @@ namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
 
-/-- Represents information about what control effects a `do` block has. -/
+/--
+Represents information about what control effects a `do` block has.
+
+The fields split by flavor:
+
+* `breaks`, `continues`, `returnsEarly`, and `reassigns` are **syntactic**: `true`/non-empty iff
+  the corresponding construct appears anywhere in the source text of the block, independent of
+  whether it is semantically reachable. Downstream elaborators must assume every such syntactic
+  effect may occur, because the elaborator visits every doElem (only top-level
+  `return`/`break`/`continue` short-circuit via `elabAsSyntacticallyDeadCode`).
+* `numRegularExits` is also **syntactic**: the number of times the block wires the enclosing
+  continuation into its elaborated expression. `withDuplicableCont` reads it as a join-point
+  duplication trigger (`> 1`).
+* `noFallthrough = true` asserts that the next doElem in the enclosing sequence is semantically
+  irrelevant (control never falls through to it). `noFallthrough = false` makes no such
+  assertion. The dead-code warning fires on the next element when this is `true`.
+
+Invariant: `numRegularExits = 0 → noFallthrough`. The converse does not hold.
+-/
 structure ControlInfo where
-  /-- The `do` block may `break`. -/
+  /-- The `do` block syntactically contains a `break`. -/
   breaks : Bool := false
-  /-- The `do` block may `continue`. -/
+  /-- The `do` block syntactically contains a `continue`. -/
   continues : Bool := false
-  /-- The `do` block may `return` early. -/
+  /-- The `do` block syntactically contains an early `return`. -/
   returnsEarly : Bool := false
   /--
-  The number of regular exit paths the `do` block has.
-  Corresponds to the number of jumps to an ambient join point.
+  The number of times the block wires the enclosing continuation into its elaborated expression.
+  Consumed by `withDuplicableCont` to decide whether to introduce a join point (`> 1`).
   -/
   numRegularExits : Nat := 1
-  /-- The variables that are reassigned in the `do` block. -/
+  /--
+  When `true`, asserts that the next doElem in the enclosing sequence is semantically irrelevant
+  (control never falls through to it). `false` asserts nothing.
+  -/
+  noFallthrough : Bool := false
+  /-- The variables that are syntactically reassigned somewhere in the `do` block. -/
   reassigns : NameSet := {}
   deriving Inhabited
 
 def ControlInfo.pure : ControlInfo := {}
 
+/--
+The identity of `ControlInfo.alternative`: a `ControlInfo` describing a block with no branches
+at all (so no regular exits and the next element is trivially unreachable).
+-/
+def ControlInfo.empty : ControlInfo := { numRegularExits := 0, noFallthrough := true }
+
 def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := {
+    -- Syntactic fields aggregate unconditionally; the elaborator keeps visiting `b` unless `a` is
+    -- a syntactically-terminal element (only top-level `return`/`break`/`continue` are, via
+    -- `elabAsSyntacticallyDeadCode`).
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    -- Once `a` has no regular exits, `b` is statically unreachable, so no regular exit survives.
-    -- We still aggregate the other effects because the elaborator keeps visiting `b` unless it is
-    -- skipped via `elabAsSyntacticallyDeadCode`.
-    numRegularExits := if a.numRegularExits == 0 then 0 else b.numRegularExits,
     reassigns := a.reassigns ++ b.reassigns,
+    numRegularExits := b.numRegularExits,
+    -- Semantic: the sequence is dead if either part is dead.
+    noFallthrough := a.noFallthrough || b.noFallthrough,
   }
 
 def ControlInfo.alternative (a b : ControlInfo) : ControlInfo := {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    numRegularExits := a.numRegularExits + b.numRegularExits,
     reassigns := a.reassigns ++ b.reassigns,
+    numRegularExits := a.numRegularExits + b.numRegularExits,
+    -- Semantic: alternatives are dead only if all branches are dead.
+    noFallthrough := a.noFallthrough && b.noFallthrough,
   }
 
 instance : ToMessageData ControlInfo where
   toMessageData info := m!"breaks: {info.breaks}, continues: {info.continues},
-    returnsEarly: {info.returnsEarly}, exitsRegularly: {info.numRegularExits},
-    reassigns: {info.reassigns.toList}"
+    returnsEarly: {info.returnsEarly}, numRegularExits: {info.numRegularExits},
+    noFallthrough: {info.noFallthrough}, reassigns: {info.reassigns.toList}"
 
 /-- A handler for inferring `ControlInfo` from a `doElem` syntax. Register with `@[doElem_control_info parserName]`. -/
 abbrev ControlInfoHandler := TSyntax `doElem → TermElabM ControlInfo
@@ -91,9 +124,9 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return ← ofElem ⟨stxNew⟩
 
   match stx with
-  | `(doElem| break) => return { breaks := true, numRegularExits := 0 }
-  | `(doElem| continue) => return { continues := true, numRegularExits := 0 }
-  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0 }
+  | `(doElem| break) => return { breaks := true, numRegularExits := 0, noFallthrough := true }
+  | `(doElem| continue) => return { continues := true, numRegularExits := 0, noFallthrough := true }
+  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0, noFallthrough := true }
   | `(doExpr| $_:term) => return { numRegularExits := 1 }
   | `(doElem| do $doSeq) => ofSeq doSeq
   -- Let
@@ -114,7 +147,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     ofLetOrReassignArrow true decl
   -- match
   | `(doElem| match $[(dependent := $_)]? $[(generalizing := $_)]? $(_)? $_,* with $alts:matchAlt*) =>
-    let mut info := {}
+    let mut info := ControlInfo.empty
     for alt in alts do
       let `(matchAltExpr| | $[$_,*]|* => $rhs) := alt | throwUnsupportedSyntax
       let rhsInfo ← ofSeq ⟨rhs⟩
@@ -132,19 +165,14 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
   -- For/Repeat
-  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
+  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq)
+  | `(doRepeat| repeat $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
       continues := false,
-      breaks := false
-    }
-  | `(doRepeat| repeat $bodySeq) =>
-    let info ← ofSeq bodySeq
-    return { info with
-      numRegularExits := if info.breaks then 1 else 0,
-      continues := false,
-      breaks := false
+      breaks := false,
+      noFallthrough := false,
     }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>

src/Lean/Linter/EnvLinter.lean

@@ -8,3 +8,4 @@ module
 prelude
 public import Lean.Linter.EnvLinter.Basic
 public import Lean.Linter.EnvLinter.Frontend
+public import Lean.Linter.EnvLinter.Builtin

src/Lean/Linter/EnvLinter/Basic.lean

@@ -13,6 +13,7 @@ prelude
 public import Lean.Structure
 public import Lean.Elab.InfoTree.Main
 import Lean.ExtraModUses
+public import Lean.Linter.EnvLinter.Nolint
 
 public section
 
@@ -135,29 +136,4 @@ builtin_initialize registerBuiltinAttribute {
     modifyEnv fun env => envLinterExt.addEntry env (decl, dflt)
 }
 
-/-- `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
-the linter with name `linterName`. -/
-syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr
-
-/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/
-builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ←
-  registerParametricAttribute {
-    name := `builtin_nolint
-    descr := "Do not report this declaration in any of the tests of `lake builtin-lint`"
-    getParam := fun _ => fun
-      | `(attr| builtin_nolint $[$ids]*) => ids.mapM fun id => withRef id <| do
-        let shortName := id.getId.eraseMacroScopes
-        let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName
-          | throwError "linter '{shortName}' not found"
-        Elab.addConstInfo id declName
-        recordExtraModUseFromDecl (isMeta := false) declName
-        pure shortName
-      | _ => Elab.throwUnsupportedSyntax
-  }
-
-/-- Returns true if `decl` should be checked
-using `linter`, i.e., if there is no `builtin_nolint` attribute. -/
-def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
-  return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter
-
 end Lean.Linter.EnvLinter

src/Lean/Linter/EnvLinter/Builtin.lean

@@ -0,0 +1,102 @@
+/-
+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 meta import Lean.Linter.EnvLinter.Basic
+public meta import Lean.MonadEnv
+public meta import Lean.ReducibilityAttrs
+public meta import Lean.ProjFns
+public meta import Lean.Meta.InferType
+public meta import Lean.Util.CollectLevelParams
+public meta import Lean.Util.ForEachExpr
+public meta import Lean.Meta.Instances
+
+open Lean Meta
+
+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.
+In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : level) ∈ e}`.
+Ignores `nm₀.proof_*` sub-constants.
+-/
+private def univParamsGrouped (e : Expr) (nm₀ : Name) : Std.HashSet (Array Name) :=
+  runST fun σ => do
+    let res ← ST.mkRef (σ := σ) {}
+    e.forEach fun
+      | .sort u =>
+        res.modify (·.insert (CollectLevelParams.visitLevel u {}).params)
+      | .const n us => do
+        if let .str n s .. := n then
+          if n == nm₀ && s.startsWith "proof_" then
+            return
+        res.modify <| us.foldl (·.insert <| CollectLevelParams.visitLevel · {} |>.params)
+      | _ => pure ()
+    res.get
+
+/--
+The good parameters are the parameters that occur somewhere in the set as a singleton or
+(recursively) with only other good parameters.
+All other parameters in the set are bad.
+-/
+private partial def badParams (l : Array (Array Name)) : Array Name :=
+  let goodLevels := l.filterMap fun
+    | #[u] => some u
+    | _ => none
+  if goodLevels.isEmpty then
+    l.flatten.toList.eraseDups.toArray
+  else
+    badParams <| l.map (·.filter (!goodLevels.contains ·))
+
+/-- A linter for checking that there are no bad `max u v` universe levels.
+Checks whether all universe levels `u` in the type of `d` are "good".
+This means that `u` either occurs in a `Level` of `d` by itself, or (recursively)
+with only other good levels.
+When this fails, usually this means that there is a level `max u v`, where neither `u` nor `v`
+occur by themselves in a level. It is ok if *one* of `u` or `v` never occurs alone. For example,
+`(α : Type u) (β : Type (max u v))` is an occasionally useful method of saying that `β` lives in
+a higher universe level than `α`. -/
+@[builtin_env_linter] def checkUnivs : EnvLinter where
+  noErrorsFound :=
+    "All declarations have good universe levels."
+  errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. \
+    This usually means that there is a `max u v` in the type where neither `u` nor `v` \
+    occur by themselves. Solution: Find the type (or type bundled with data) that has this \
+    universe argument and provide the universe level explicitly. If this happens in an implicit \
+    argument of the declaration, a better solution is to move this argument to a `variables` \
+    command (then it's not necessary to provide the universe level).\n\n\
+    It is possible that this linter gives a false positive on definitions where the value of the \
+    definition has the universes occur separately, and the definition will usually be used with \
+    explicit universe arguments. In this case, feel free to add `@[builtin_nolint checkUnivs]`."
+  test declName := do
+    if ← isAutoDecl declName then return none
+    let bad := badParams (univParamsGrouped (← getConstInfo declName).type declName).toArray
+    if bad.isEmpty then return none
+    return m!"universes {bad} only occur together."
+
+end Lean.Linter.EnvLinter
+
+end

src/Lean/Linter/EnvLinter/Frontend.lean

@@ -32,18 +32,33 @@ inductive LintVerbosity
   | high
   deriving Inhabited, DecidableEq, Repr
 
-/-- `getChecks clippy runOnly` produces a list of linters.
-`runOnly` is an optional list of names that should resolve to declarations with type
-`NamedEnvLinter`. If populated, only these linters are run (regardless of the default
-configuration). Otherwise, it uses all enabled linters in the environment tagged with
-`@[builtin_env_linter]`. If `clippy` is false, it only uses linters with `isDefault = true`. -/
-def getChecks (clippy : Bool) (runOnly : Option (List Name)) :
+/-- Which set of linters to run. -/
+inductive LintScope
+  /-- Run only default linters. -/
+  | default
+  /-- Run only non-default (clippy) linters. -/
+  | clippy
+  /-- Run all linters (default + clippy). -/
+  | all
+  deriving Inhabited, DecidableEq, Repr
+
+/-- `getChecks` produces a list of linters to run.
+
+If `runOnly` is populated, only those named linters are run (regardless of `scope`).
+Otherwise, linter selection depends on `scope`:
+- `default`: only linters with `isDefault = true`
+- `clippy`: only linters with `isDefault = false`
+- `all`: all linters -/
+def getChecks (scope : LintScope := .default) (runOnly : Option (List Name) := none) :
     CoreM (Array NamedEnvLinter) := do
   let mut result := #[]
   for (name, declName, isDefault) in envLinterExt.getState (← getEnv) do
     let shouldRun := match runOnly with
       | some only => only.contains name
-      | none => clippy || isDefault
+      | none => match scope with
+        | .default => isDefault
+        | .clippy => !isDefault
+        | .all => true
     if shouldRun then
       let linter ← getEnvLinter name declName
       result := result.binInsert (·.name.lt ·.name) linter
@@ -133,7 +148,7 @@ def formatLinterResults
     (results : Array (NamedEnvLinter × Std.HashMap Name MessageData))
     (decls : Array Name)
     (groupByFilename : Bool)
-    (whereDesc : String) (runClippyLinters : Bool)
+    (whereDesc : String) (scope : LintScope := .default)
     (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) :
     CoreM MessageData := do
   let formattedResults ← results.filterMapM fun (linter, results) => do
@@ -156,7 +171,10 @@ def formatLinterResults
       } in {decls.size - numAutoDecls} declarations (plus {
       numAutoDecls} automatically generated ones) {whereDesc
       } with {numLinters} linters\n\n{s}"
-  unless runClippyLinters do s := m!"{s}-- (non-clippy linters skipped)\n"
+  match scope with
+  | .default => s := m!"{s}-- (non-default linters skipped)\n"
+  | .clippy => s := m!"{s}-- (default linters skipped)\n"
+  | .all => pure ()
   pure s
 
 /-- Get the list of declarations in the current module. -/

src/Lean/Linter/EnvLinter/Nolint.lean

@@ -0,0 +1,35 @@
+/-
+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.Attributes
+import Init.Linter
+
+public section
+
+namespace Lean.Linter.EnvLinter
+
+/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/
+builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ←
+  registerParametricAttribute {
+    name := `builtin_nolint
+    descr := "Do not report this declaration in any of the tests of `lake builtin-lint`"
+    getParam := fun _ => fun
+      | `(attr| builtin_nolint $[$ids]*) => pure <| ids.map (·.getId.eraseMacroScopes)
+      | _ => Elab.throwUnsupportedSyntax
+  }
+
+/-- Returns true if `decl` should be checked
+using `linter`, i.e., if there is no `builtin_nolint` attribute. -/
+def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
+  return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter
+
+end Lean.Linter.EnvLinter

src/lake/Lake/CLI/BuiltinLint.lean

@@ -0,0 +1,69 @@
+/-
+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
+-/
+module
+
+prelude
+public import Lean.Linter.EnvLinter
+import Lean.CoreM
+import Lake.Config.Workspace
+
+open Lean Lean.Core Meta
+
+namespace Lake.BuiltinLint
+
+/-- Arguments for builtin linting via `lake lint --builtin-lint`. -/
+public structure Args where
+  /-- Which set of linters to run (set by `--clippy` / `--lint-all`; default if neither). -/
+  scope : Linter.EnvLinter.LintScope := .default
+  /-- Run only the specified linters. -/
+  only : Array Name := #[]
+  /-- Skip the up-to-date build check. -/
+  force : Bool := false
+  /-- The list of root modules to lint. -/
+  mods : Array Name := #[]
+
+/--
+Run the builtin environment linters on the given modules.
+
+Assumes Lean's search path has already been properly configured.
+-/
+public def run (args : Args) : IO UInt32 := do
+  let mods := args.mods
+  if mods.isEmpty then
+    IO.eprintln "lake lint: no modules specified for builtin linting"
+    return 1
+
+  let runOnly := if args.only.isEmpty then none else some args.only.toList
+  let scope := args.scope
+  let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
+
+  let mut anyFailed := false
+  for mod in mods do
+    unsafe Lean.enableInitializersExecution
+    let env ← importModules #[{ module := mod }, envLinterModule] {} (trustLevel := 1024) (loadExts := true)
+    let (result, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
+      let decls ← Linter.EnvLinter.getDeclsInPackage mod.getRoot
+      let linters ← Linter.EnvLinter.getChecks (scope := scope) (runOnly := runOnly)
+      if linters.isEmpty then
+        IO.println s!"-- No linters registered for {mod}."
+        return false
+      let results ← Linter.EnvLinter.lintCore decls linters
+      let failed := results.any (!·.2.isEmpty)
+      if failed then
+        let fmtResults ←
+          Linter.EnvLinter.formatLinterResults results decls
+            (groupByFilename := true) (useErrorFormat := true)
+            s!"in {mod}" (scope := if args.only.isEmpty then scope else .all) .medium linters.size
+        IO.print (← fmtResults.toString)
+      else
+        IO.println s!"-- Linting passed for {mod}."
+      return failed
+    if result then
+      anyFailed := true
+
+  return if anyFailed then 1 else 0
+
+end Lake.BuiltinLint

src/lake/Lake/CLI/Help.lean

@@ -26,7 +26,7 @@ COMMANDS:
   check-build           check if any default build targets are configured
   test                  test the package using the configured test driver
   check-test            check if there is a properly configured test driver
-  lint                  lint the package using the configured lint driver
+  lint                  lint the package
   check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   shake                 minimize imports in source files
@@ -242,17 +242,33 @@ package or its dependencies. It merely verifies that one is specified.
 "
 
 def helpLint :=
-"Lint the workspace's root package using its configured lint driver
+"Lint the workspace's root package
 
 USAGE:
-  lake lint [-- <args>...]
+  lake lint [OPTIONS] [<MODULE>...] [-- <args>...]
+
+By default, runs the package's configured lint driver. If `builtinLint` is
+set to `true` in the package configuration, builtin lints also run.
+
+Positional `MODULE` arguments narrow only the builtin lints; if omitted,
+the workspace's default target roots are used. The lint driver is invoked
+with `lintDriverArgs` from the package config plus any arguments after
+`--`; the `MODULE` list is not passed to it.
+
+OPTIONS:
+  --builtin-lint        run builtin environment linters
+  --builtin-only        run only builtin linters, skip the lint driver
+  --clippy              run only non-default (clippy) builtin linters
+  --lint-all            run all builtin linters (default + clippy)
+  --lint-only <name>    run only the specified builtin linter (repeatable)
+  --force               skip the up-to-date build check
 
 A lint driver can be configured by either setting the `lintDriver` package
-configuration option by tagging a script or executable `@[lint_driver]`.
-A definition in dependency can be used as a test driver by using the
-`<pkg>/<name>` syntax for the 'testDriver' configuration option.
+configuration option or by tagging a script or executable `@[lint_driver]`.
+A definition in a dependency can be used as a lint driver by using the
+`<pkg>/<name>` syntax for the 'lintDriver' configuration option.
 
-A script lint driver will be run with the  package configuration's
+A script lint driver will be run with the package configuration's
 `lintDriverArgs` plus the CLI `args`. An executable lint driver will be
 built and then run like a script.
 "

src/lake/Lake/CLI/Main.lean

@@ -27,6 +27,7 @@ import Lake.CLI.Build
 import Lake.CLI.Actions
 import Lake.CLI.Translate
 import Lake.CLI.Serve
+public import Lake.CLI.BuiltinLint
 import Init.Data.String.Modify
 
 -- # CLI
@@ -72,6 +73,11 @@ public structure LakeOptions where
   rev? : Option GitRev := none
   maxRevs : Nat := 100
   shake : Shake.Args := {}
+  builtinLint : BuiltinLint.Args := {}
+  /-- Whether `lake lint` should also run builtin lints (via `--builtin-lint`). -/
+  runBuiltinLint : Bool := false
+  /-- Whether `lake lint` should skip the lint driver (via `--builtin-only`). -/
+  builtinOnly : Bool := false
 
 def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
   opts.outLv?.getD opts.verbosity.minLogLv
@@ -302,12 +308,24 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--"            => do
   let subArgs ← takeArgs
   modifyThe LakeOptions ({· with subArgs})
+-- Builtin lint options (using any of these implicitly enables --builtin-lint)
+| "--builtin-lint" => modifyThe LakeOptions ({· with runBuiltinLint := true})
+| "--builtin-only" => modifyThe LakeOptions ({· with runBuiltinLint := true, builtinOnly := true})
+| "--clippy" => modifyThe LakeOptions ({· with
+    runBuiltinLint := true, builtinLint.scope := .clippy, builtinLint.only := #[]})
+| "--lint-all" => modifyThe LakeOptions ({· with
+    runBuiltinLint := true, builtinLint.scope := .all, builtinLint.only := #[]})
+| "--lint-only" => do
+  let name ← takeOptArg "--lint-only" "linter name"
+  modifyThe LakeOptions fun opts =>
+    {opts with runBuiltinLint := true, builtinLint.only := opts.builtinLint.only.push name.toName}
+-- Shared options
+| "--force" => modifyThe LakeOptions ({· with shake.force := true, builtinLint.force := true})
 -- Shake options
 | "--keep-implied" => modifyThe LakeOptions ({· with shake.keepImplied := true})
 | "--keep-prefix" => modifyThe LakeOptions ({· with shake.keepPrefix := true})
 | "--keep-public" => modifyThe LakeOptions ({· with shake.keepPublic := true})
 | "--add-public" => modifyThe LakeOptions ({· with shake.addPublic := true})
-| "--force" => modifyThe LakeOptions ({· with shake.force := true})
 | "--gh-style" => modifyThe LakeOptions ({· with shake.githubStyle := true})
 | "--explain" => modifyThe LakeOptions ({· with shake.explain := true})
 | "--trace" => modifyThe LakeOptions ({· with shake.trace := true})
@@ -945,18 +963,46 @@ protected def checkTest : CliM PUnit := do
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
   noArgsRem do exit <| if pkg.testDriver.isEmpty then 1 else 0
 
+private def runBuiltinLint
+    (ws : Workspace) (args : BuiltinLint.Args) (mods : Array Lean.Name) : CliM UInt32 := do
+  let mods := if mods.isEmpty then ws.defaultTargetRoots else mods
+  if mods.isEmpty then
+    error "no modules specified and there are no applicable default targets"
+  let args := {args with mods}
+  unless args.force do
+    let specs ← parseTargetSpecs ws (mods.map (s!"+{·}") |>.toList)
+    let upToDate ← ws.checkNoBuild <| buildSpecs specs
+    unless upToDate do
+      error "there are out of date oleans; run `lake build` or fetch them from a cache first"
+  Lean.searchPathRef.set ws.augmentedLeanPath
+  BuiltinLint.run args
+
 protected def lint : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let ws ← loadWorkspace (← mkLoadConfig opts)
-  noArgsRem do
-  let x := ws.root.lint opts.subArgs (mkBuildConfig opts)
-  exit <| ← x.run (mkLakeContext ws)
+  let hasDriver := !ws.root.lintDriver.isEmpty && !opts.builtinOnly
+  let pkgBuiltinLint := ws.root.config.builtinLint?
+  let doBuiltinLint := opts.runBuiltinLint || pkgBuiltinLint == some true
+  let mut exitCode : UInt32 := 0
+  if doBuiltinLint then
+    let mods := (← takeArgs).toArray.map (·.toName)
+    exitCode ← runBuiltinLint ws opts.builtinLint mods
+  if hasDriver then
+    let driverExitCode ← noArgsRem do
+      ws.root.lint opts.subArgs (mkBuildConfig opts) |>.run (mkLakeContext ws)
+    unless driverExitCode == 0 do
+      exitCode := driverExitCode
+  unless doBuiltinLint || hasDriver do
+    error s!"no lint driver configured and builtin linting is disabled"
+  exit exitCode
 
 protected def checkLint : CliM PUnit := do
   processOptions lakeOption
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
-  noArgsRem do exit <| if pkg.lintDriver.isEmpty then 1 else 0
+  noArgsRem do
+  let hasLint := !pkg.lintDriver.isEmpty || pkg.config.builtinLint? == some true
+  exit <| if hasLint then 0 else 1
 
 protected def clean : CliM PUnit := do
   processOptions lakeOption

src/lake/Lake/Config/PackageConfig.lean

@@ -321,6 +321,19 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   -/
   allowImportAll : Bool := false
 
+  /--
+  Whether to run Lake's built-in linter on the package.
+
+  * `true` — Always run built-in lints. When a lint driver is also configured,
+    built-in lints run before the driver.
+  * `false` — Never run built-in lints by default. `lake check-lint` will exit
+    with a nonzero code if no lint driver is configured either.
+  * `none` (default) — Currently equivalent to `false`. In a future release, `none`
+    will run built-in lints when no lint driver is configured (i.e., act like `true`
+    as a fallback).
+  -/
+  builtinLint?, builtinLint : Option Bool := none
+
   /--
   Whether this package is expected to function only on a single toolchain
   (the package's toolchain).

src/lake/Lake/Load/Resolve.lean

@@ -163,7 +163,7 @@ See `Workspace.updateAndMaterializeCore` for more details.
 @[inline] def Workspace.resolveDepsCore
   [Monad m] [MonadError m] [MonadLiftT LogIO m] (ws : Workspace)
   (resolve : Package → Dependency → Workspace → m MaterializedDep)
-  (root : Nat := 0) (h : root < ws.packages.size := by exact ws.size_packages_pos)
+  (root : Nat) (h : root < ws.packages.size)
   (leanOpts : Options := {}) (reconfigure := true)
 : m (MinWorkspace ws) := do
   go ws root h
@@ -473,7 +473,7 @@ def Workspace.updateAndMaterializeCore
     -- that the dependencies' dependencies are also properly set
     return ws.setDepPkgs ws.root ws.packages[start...<stop] ws.wsIdx_root_lt
   else
-    ws.resolveDepsCore updateAndAddDep (leanOpts := leanOpts) (reconfigure := true)
+    ws.resolveDepsCore updateAndAddDep ws.root.wsIdx ws.wsIdx_root_lt leanOpts (reconfigure := true)
 where
   @[inline] updateAndAddDep pkg dep ws := do
     let matDep ← updateAndMaterializeDep ws pkg dep
@@ -570,7 +570,7 @@ public def Workspace.materializeDeps
   if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
     error "missing manifest; use `lake update` to generate one"
   -- Materialize all dependencies
-  ws.resolveDepsCore (leanOpts := leanOpts) (reconfigure := reconfigure) fun pkg dep ws => do
+  let materialize pkg dep ws := do
     if let some entry := pkgEntries.find? dep.name then
       entry.materialize ws.lakeEnv ws.dir relPkgsDir
     else
@@ -584,3 +584,4 @@ public def Workspace.materializeDeps
           this suggests that the manifest is corrupt; \
           use `lake update` to generate a new, complete file \
           (warning: this will update ALL workspace dependencies)"
+  ws.resolveDepsCore materialize ws.root.wsIdx ws.wsIdx_root_lt leanOpts reconfigure

src/lake/schemas/lakefile-toml-schema.json

@@ -568,6 +568,10 @@
                     "default": [],
                     "description": "Arguments to pass to the package's linter.\nThese arguments will come before those passed on the command line via `lake lint -- <args>...`."
                 },
+                "builtinLint": {
+                    "type": "boolean",
+                    "description": "Whether to run Lake's built-in linter on the package.\n\n* `true` — Always run built-in lints. When a lint driver is also configured, built-in lints run before the driver.\n* `false` — Never run built-in lints by default. `lake check-lint` will exit with a nonzero code if no lint driver is configured either.\n* unset (the default) — Currently equivalent to `false`. In a future release, an unset value will run built-in lints when no lint driver is configured (i.e., act like `true` as a fallback)."
+                },
                 "releaseRepo": {
                     "type": "string",
                     "description": "The URL of the GitHub repository to upload and download releases of this package.\nIf not set, for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default."

tests/CMakeLists.txt

@@ -261,6 +261,7 @@ else()
     GLOB_RECURSE LEANLAKETESTS
     "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
     "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh"
+    "${LEAN_SOURCE_DIR}/../tests/lake/tests/builtin-lint/test.sh"
   )
 endif()
 foreach(T ${LEANLAKETESTS})

tests/bench/mvcgen/sym/run_test.sh

@@ -1,2 +1 @@
-# Limit threads to avoid exhausting memory with the large thread stack.
-LEAN_NUM_THREADS=1 lake test
+lake test

tests/elab/doControlInfoAggregate.lean

@@ -28,6 +28,9 @@ example (cond : Bool) : IO Nat := do
     return 42
   return 1
 
+/--
+warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
+-/
 #guard_msgs in
 example (i : Nat) : IO Nat := do
   for _ in [1, 2] do
@@ -65,3 +68,15 @@ example : IO Nat := do
       pure ()
     return 42
   return 1
+
+-- The `return 2` is required to give the do block its `Id Nat` result type; no dead-code warning
+-- should fire on it.
+#guard_msgs in
+example (x : Nat) : Id Nat := do
+  if x = 3 then
+    repeat
+      pure ()
+  else
+    repeat
+      pure ()
+  return 2

tests/elab/env_linter.lean

@@ -127,26 +127,35 @@ error: invalid attribute `builtin_env_linter`, linter `dummyBadName` has already
 
 -- Default mode: only isDefault=true linters
 def testGetChecksDefault : CoreM (Array Name) := do
-  let checks ← getChecks (clippy := false) (runOnly := none)
+  let checks ← getChecks (scope := .default) (runOnly := none)
   return checks.map (·.name)
 
--- dummyBadName is default, dummyClippyLinter is not
-/-- info: #[`dummyBadName] -/
+-- dummyBadName and checkUnivs are default, dummyClippyLinter is not
+/-- info: #[`checkUnivs, `defLemma, `dummyBadName] -/
 #guard_msgs in
 #eval testGetChecksDefault
 
--- Clippy mode: all linters
+-- Clippy mode: only non-default linters
 def testGetChecksClippy : CoreM (Array Name) := do
-  let checks ← getChecks (clippy := true) (runOnly := none)
+  let checks ← getChecks (scope := .clippy) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`dummyBadName, `dummyClippyLinter] -/
+/-- info: #[`dummyClippyLinter] -/
 #guard_msgs in
 #eval testGetChecksClippy
 
+-- All mode: all linters
+def testGetChecksAll : CoreM (Array Name) := do
+  let checks ← getChecks (scope := .all) (runOnly := none)
+  return checks.map (·.name)
+
+/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyClippyLinter] -/
+#guard_msgs in
+#eval testGetChecksAll
+
 -- runOnly: only specified linters
 def testGetChecksRunOnly : CoreM (Array Name) := do
-  let checks ← getChecks (clippy := false) (runOnly := some [`dummyClippyLinter])
+  let checks ← getChecks (runOnly := some [`dummyClippyLinter])
   return checks.map (·.name)
 
 /-- info: #[`dummyClippyLinter] -/
@@ -168,17 +177,17 @@ def testDeclsInCurrModule : CoreM Bool := do
 
 -- lintCore should find badDef but not goodDef or badButNolinted
 def testLintCore : CoreM (Array (Name × Nat)) := do
-  let linters ← getChecks (clippy := false) (runOnly := none)
+  let linters ← getChecks (scope := .default) (runOnly := none)
   let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
   return results.map fun (linter, msgs) => (linter.name, msgs.size)
 
-/-- info: #[(`dummyBadName, 1)] -/
+/-- info: #[(`checkUnivs, 0), (`defLemma, 0), (`dummyBadName, 1)] -/
 #guard_msgs in
 #eval testLintCore
 
 -- Verify which declaration was flagged
 def testLintCoreDetail : CoreM (Array Name) := do
-  let linters ← getChecks (clippy := false) (runOnly := none)
+  let linters ← getChecks (scope := .default) (runOnly := none)
   let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
   let mut flagged := #[]
   for (_, msgs) in results do
@@ -193,15 +202,15 @@ def testLintCoreDetail : CoreM (Array Name) := do
 /-! ## Test: formatLinterResults -/
 
 def testFormatResults : CoreM Format := do
-  let linters ← getChecks (clippy := false) (runOnly := none)
+  let linters ← getChecks (scope := .default) (runOnly := none)
   let results ← lintCore #[`badDef, `goodDef] linters
   let msg ← formatLinterResults results #[`badDef, `goodDef]
-    (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
+    (groupByFilename := false) (whereDesc := "in test") (scope := .all)
     (verbose := .medium) (numLinters := linters.size)
   return (← msg.format)
 
 /--
-info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 1 linters
+info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 3 linters
 
 /- The `dummyBadName` linter reports:
 found bad names -/
@@ -212,15 +221,47 @@ found bad names -/
 
 -- No errors case
 def testFormatResultsClean : CoreM Format := do
-  let linters ← getChecks (clippy := false) (runOnly := none)
+  let linters ← getChecks (scope := .default) (runOnly := none)
   let results ← lintCore #[`goodDef] linters
   let msg ← formatLinterResults results #[`goodDef]
-    (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
+    (groupByFilename := false) (whereDesc := "in test") (scope := .all)
     (verbose := .medium) (numLinters := linters.size)
   return (← msg.format)
 
 /--
-info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 1 linters
+info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 3 linters
 -/
 #guard_msgs in
 #eval testFormatResultsClean
+
+/-! ## Test: checkUnivs -/
+
+-- Good: each universe parameter occurs alone somewhere
+universe u v in
+def goodUnivs (α : Type u) (β : Type v) : Type (max u v) := α × β
+
+-- Good: one universe dominates the other (max u v where u occurs alone)
+universe u v in
+def goodUnivsDominated (α : Type u) (β : Type (max u v)) : Type (max u v) := α × β
+
+-- Bad: neither u nor v occur alone
+universe u v in
+def badUnivs (α : Type (max u v)) : Type (max u v) := α
+
+def testCheckUnivs (declName : Name) : MetaM Bool := do
+  let some (linterDeclName, _) := (envLinterExt.getState (← getEnv)).find? `checkUnivs
+    | throwError "not found"
+  let linter ← getEnvLinter `checkUnivs linterDeclName
+  return (← linter.test declName).isSome
+
+/-- info: false -/
+#guard_msgs in
+#eval testCheckUnivs `goodUnivs
+
+/-- info: false -/
+#guard_msgs in
+#eval testCheckUnivs `goodUnivsDominated
+
+/-- info: true -/
+#guard_msgs in
+#eval testCheckUnivs `badUnivs

tests/lake/tests/builtin-lint/Clean.lean

@@ -0,0 +1,4 @@
+-- No linter violations here.
+theorem correctTheorem : 1 = 1 := rfl
+
+def correctDef : Nat := 42

tests/lake/tests/builtin-lint/ClippyViolations.lean

@@ -0,0 +1,4 @@
+import Linters
+
+-- This name ends with 'Clippy' — the dummyClippy linter should flag it.
+def badNameClippy : Nat := 1

tests/lake/tests/builtin-lint/Linters.lean

@@ -0,0 +1,12 @@
+import Lean.Linter.EnvLinter
+
+open Lean Meta
+
+-- A dummy clippy linter that flags any declaration whose name ends with "Clippy".
+@[builtin_env_linter clippy] public meta def dummyClippy : Lean.Linter.EnvLinter.EnvLinter where
+  noErrorsFound := "No declarations ending with 'Clippy' found."
+  errorsFound := "CLIPPY VIOLATIONS:"
+  test declName := do
+    if declName.toString.endsWith "Clippy" then
+      return some "declaration name ends with 'Clippy'"
+    return none

tests/lake/tests/builtin-lint/Main.lean

@@ -0,0 +1,24 @@
+-- This uses `def` for a Prop — the `defLemma` linter should flag this.
+def shouldBeTheorem : 1 = 1 := rfl
+
+-- This is annotated to be skipped by `defLemma` — no import needed.
+@[builtin_nolint defLemma]
+def skippedViolation : 2 = 2 := rfl
+
+-- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`,
+-- so `defLemma` should flag it.
+@[reducible, instance]
+def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩
+
+-- A plain `instance` of Prop type is elaborated as a `theorem`, so it should
+-- not be flagged.
+instance plainInstIsOk : Nonempty String := ⟨""⟩
+
+-- Bad universe levels — the `checkUnivs` linter should flag this.
+universe u v in
+def badUnivDecl (α : Type (max u v)) : Type (max u v) := α
+
+-- Annotated to be skipped by `checkUnivs`.
+universe u v in
+@[builtin_nolint checkUnivs]
+def badUnivSkipped (α : Type (max u v)) : Type (max u v) := α

tests/lake/tests/builtin-lint/clean.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+rm -rf .lake
+rm -f lakefile.toml lake-manifest.json Main.lean Clean.lean Linters.lean ClippyViolations.lean

tests/lake/tests/builtin-lint/input/Clean.lean

@@ -0,0 +1,4 @@
+-- No linter violations here.
+theorem correctTheorem : 1 = 1 := rfl
+
+def correctDef : Nat := 42

tests/lake/tests/builtin-lint/input/ClippyViolations.lean

@@ -0,0 +1,4 @@
+import Linters
+
+-- This name ends with 'Clippy' — the dummyClippy linter should flag it.
+def badNameClippy : Nat := 1

tests/lake/tests/builtin-lint/input/Linters.lean

@@ -0,0 +1,12 @@
+import Lean.Linter.EnvLinter
+
+open Lean Meta
+
+-- A dummy clippy linter that flags any declaration whose name ends with "Clippy".
+@[builtin_env_linter clippy] public meta def dummyClippy : Lean.Linter.EnvLinter.EnvLinter where
+  noErrorsFound := "No declarations ending with 'Clippy' found."
+  errorsFound := "CLIPPY VIOLATIONS:"
+  test declName := do
+    if declName.toString.endsWith "Clippy" then
+      return some "declaration name ends with 'Clippy'"
+    return none

tests/lake/tests/builtin-lint/input/Main.lean

@@ -0,0 +1,24 @@
+-- This uses `def` for a Prop — the `defLemma` linter should flag this.
+def shouldBeTheorem : 1 = 1 := rfl
+
+-- This is annotated to be skipped by `defLemma` — no import needed.
+@[builtin_nolint defLemma]
+def skippedViolation : 2 = 2 := rfl
+
+-- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`,
+-- so `defLemma` should flag it.
+@[reducible, instance]
+def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩
+
+-- A plain `instance` of Prop type is elaborated as a `theorem`, so it should
+-- not be flagged.
+instance plainInstIsOk : Nonempty String := ⟨""⟩
+
+-- Bad universe levels — the `checkUnivs` linter should flag this.
+universe u v in
+def badUnivDecl (α : Type (max u v)) : Type (max u v) := α
+
+-- Annotated to be skipped by `checkUnivs`.
+universe u v in
+@[builtin_nolint checkUnivs]
+def badUnivSkipped (α : Type (max u v)) : Type (max u v) := α

tests/lake/tests/builtin-lint/input/lakefile.toml

@@ -0,0 +1,14 @@
+name = "lint"
+defaultTargets = ["Main", "Clean", "Linters", "ClippyViolations"]
+
+[[lean_lib]]
+name = "Main"
+
+[[lean_lib]]
+name = "Clean"
+
+[[lean_lib]]
+name = "Linters"
+
+[[lean_lib]]
+name = "ClippyViolations"

tests/lake/tests/builtin-lint/lakefile.toml

@@ -0,0 +1,14 @@
+name = "lint"
+defaultTargets = ["Main", "Clean", "Linters", "ClippyViolations"]
+
+[[lean_lib]]
+name = "Main"
+
+[[lean_lib]]
+name = "Clean"
+
+[[lean_lib]]
+name = "Linters"
+
+[[lean_lib]]
+name = "ClippyViolations"

tests/lake/tests/builtin-lint/lean-toolchain

@@ -0,0 +1 @@
+../../../../../build/release/stage1

tests/lake/tests/builtin-lint/test.sh

@@ -0,0 +1,148 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+cp -r input/* .
+
+# --builtin-lint should fail with a clear message when oleans are not built
+lake_out lint --builtin-lint || true
+match_pat 'out of date oleans' produced.out
+
+# up-to-date check is per-module: building only Clean should let us lint Clean
+test_run build Clean
+test_run lint --builtin-only Clean
+
+# but linting Main (not yet built) should still fail the up-to-date check
+lake_out lint --builtin-only Main || true
+match_pat 'out of date oleans' produced.out
+
+test_run build
+
+# --builtin-lint should detect the defLemma 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
+# `@[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.
+no_match_pat 'plainInstIsOk' produced.out
+
+# --builtin-lint should also detect the checkUnivs violation
+match_pat 'badUnivDecl' produced.out
+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
+match_pat 'shouldBeTheorem' produced.out
+no_match_pat 'badUnivDecl' produced.out
+
+# Clean module has no violations; exit code should be 0
+test_run lint --builtin-only Clean
+
+# Without --clippy, the clippy linter should not run
+lake_out lint --builtin-only ClippyViolations || true
+no_match_pat 'badNameClippy' produced.out
+
+# --clippy should run only non-default (clippy) linters
+lake_out lint --clippy ClippyViolations || true
+match_pat 'badNameClippy' produced.out
+match_pat "declaration name ends with 'Clippy'" produced.out
+# --clippy should not run default linters
+no_match_pat 'shouldBeTheorem' produced.out
+
+# --lint-all should run both default and clippy linters
+lake_out lint --lint-all ClippyViolations || true
+match_pat 'badNameClippy' produced.out
+
+# Multiple --lint-only flags accumulate: both named linters should run
+lake_out lint --lint-only defLemma --lint-only checkUnivs || true
+match_pat 'shouldBeTheorem' produced.out
+match_pat 'badUnivDecl' produced.out
+no_match_pat 'badNameClippy' produced.out
+
+# Last-wins: --clippy overrides a prior --lint-all and clears --lint-only
+lake_out lint --lint-all --lint-only defLemma --clippy || true
+match_pat 'badNameClippy' produced.out
+no_match_pat 'shouldBeTheorem' produced.out
+no_match_pat 'badUnivDecl' produced.out
+
+# Last-wins: --lint-all overrides a prior --clippy (both default and clippy run)
+lake_out lint --clippy --lint-all || true
+match_pat 'badNameClippy' produced.out
+match_pat 'shouldBeTheorem' produced.out
+
+# Last-wins: --clippy clears a previously accumulated --lint-only
+lake_out lint --lint-only defLemma --clippy || true
+match_pat 'badNameClippy' produced.out
+no_match_pat 'shouldBeTheorem' produced.out
+
+# --lint-only after --clippy: the named linter runs (selection ignores scope)
+lake_out lint --clippy --lint-only defLemma || true
+match_pat 'shouldBeTheorem' produced.out
+no_match_pat 'badNameClippy' produced.out
+
+# --builtin-only should skip the lint driver
+lake_out lint -f with-driver.lean --builtin-only Main || true
+match_pat 'shouldBeTheorem' produced.out
+no_match_pat 'lint-driver:' produced.out
+
+# --- builtinLint package configuration tests ---
+
+# Default (builtinLint unset / none): check-lint fails (same as false for now)
+test_fails check-lint
+
+# Default: lake lint errors when no lintDriver and builtinLint is unset
+lake_out lint || true
+match_pat 'no lint driver configured' produced.out
+
+# Default: lake lint --builtin-lint overrides and runs builtin lints
+lake_out lint --builtin-lint || true
+match_pat 'shouldBeTheorem' produced.out
+
+# --clippy implicitly enables builtin lint
+lake_out lint --clippy ClippyViolations || true
+match_pat 'badNameClippy' produced.out
+
+# --lint-only implicitly enables builtin lint
+lake_out lint --lint-only defLemma || true
+match_pat 'shouldBeTheorem' produced.out
+
+# builtinLint = false: check-lint fails (no lint driver and builtin linting disabled)
+sed_i 's/^name = .*/&\nbuiltinLint = false/' lakefile.toml
+test_fails check-lint
+
+# builtinLint = false: lake lint errors
+lake_out lint || true
+match_pat 'no lint driver configured' produced.out
+
+# builtinLint = false with --builtin-lint flag: overrides and runs builtin lints
+lake_out lint --builtin-lint || true
+match_pat 'shouldBeTheorem' produced.out
+
+# builtinLint = true: check-lint succeeds even without a lint driver
+sed_i 's/builtinLint = false/builtinLint = true/' lakefile.toml
+test_run check-lint
+
+# builtinLint = true: lake lint runs builtin lints
+lake_out lint || true
+match_pat 'shouldBeTheorem' produced.out
+
+# Restore original lakefile
+cp input/lakefile.toml lakefile.toml
+
+# --- builtinLint = true with a lint driver ---
+
+# builtinLint = true + lint driver + clean module: both builtin lints and driver run
+lake_out lint -f with-driver.lean Clean || true
+match_pat 'Linting passed for Clean' produced.out
+match_pat 'lint-driver:' produced.out
+
+# builtinLint = true + lint driver + violations: both run, exit code is nonzero
+lake_out lint -f with-driver.lean Main || true
+match_pat 'shouldBeTheorem' produced.out
+match_pat 'lint-driver:' produced.out
+
+# builtinLint = true + lint driver: check-lint succeeds
+test_run -f with-driver.lean check-lint

tests/lake/tests/builtin-lint/with-driver.lean

@@ -0,0 +1,15 @@
+import Lake
+open System Lake DSL
+
+package lint where
+  builtinLint := true
+
+@[lint_driver]
+script lintDriver args do
+  IO.println s!"lint-driver: {args}"
+  return 0
+
+lean_lib Main
+lean_lib Clean
+lean_lib Linters
+lean_lib ClippyViolations

tests/pkg/homo/Homo.lean

@@ -0,0 +1,25 @@
+import Homo.Init
+
+set_option warn.sorry false
+
+opaque TSpec : (α : Type) × α := ⟨Unit, ()⟩
+abbrev T : Type := TSpec.1
+instance : Inhabited T := ⟨TSpec.2⟩
+opaque add : T → T → T
+opaque le : T → T → Prop
+opaque pos : T → Prop
+opaque small : T → Prop
+opaque f : Nat → T
+opaque toInt : T → Int
+
+@[grind_homo] theorem T.eq (a b : T) : a = b ↔ toInt a = toInt b := sorry
+@[grind_homo] theorem T.le (a b : T) : le a b ↔ toInt a ≤ toInt b := sorry
+@[grind_homo] theorem T.pos (a : T) : pos a ↔ toInt a > 0 := sorry
+@[grind_homo] theorem T.small (a : T) : small a ↔ toInt a < 8 := sorry
+@[grind_homo] theorem T.add (a b : T) : toInt (add a b) = (toInt a + toInt b) % 128 := sorry
+@[grind_homo] theorem cleanLeft (a b n : Int) : (a % n + b) % n = (a + b) % n := by simp
+@[grind_homo] theorem cleanRight (a b n : Int) : (a + b % n) % n = (a + b) % n := by simp
+
+set_option trace.homo true
+example (b : T) : pos b → small b → le b (add b b) := by
+  grind

tests/pkg/homo/Homo/Init.lean

@@ -0,0 +1,96 @@
+module
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Sym.Simp.Attr
+import Lean.Meta.Sym.Simp.Simproc
+import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.AppBuilder
+
+namespace Homomorphism
+
+open Lean Meta Grind Sym Simp
+
+initialize registerTraceClass `homo
+initialize registerTraceClass `homo.visit
+
+/--
+Declares attribute `[grind_mono]` for marking theorems implementing the homomorphism.
+-/
+initialize homoSimpExtension : SymSimpExtension ←
+  registerSymSimpAttr `grind_homo "`grind` homomorphism attribute"
+
+/--
+Returns theorems marked with `[grind_mono]`
+-/
+def getTheorems : CoreM Theorems :=
+  homoSimpExtension.getTheorems
+
+/--
+Creates a simproc that applies the theorems marked with `[grind_mono]`.
+This simproc is meant to be applied as a `pre` method.
+
+Recall that `grind` internalizes terms bottom-up. By the time a
+simplification set runs on a term `e`, all subterms of `e` are already
+in the E-graph and have been processed by the pipeline.
+
+**Stop condition.** When simp encounters a term `t` during traversal:
+
+- If a rule matches `t`: apply it, continue (result is a new term).
+- If no rule matches `t` AND `t` is already in the E-graph:
+  stop, don't descend. Otherwise: descend normally.
+-/
+def mkRewriter : GoalM Sym.Simp.Simproc := do
+  let s ← get
+  -- Remark: We are not using any discharger. So, our rewriting rules are all context
+  -- independent.
+  let rw := (← getTheorems).rewrite
+  return fun e => do
+    trace[homo.visit] "{e}"
+    let r ← rw e
+    if !r.isRfl then return r
+    -- If `e` is already in the E-graph, we don't revisit its children
+    let done := s.enodeMap.contains { expr := e }
+    return .rfl (done := done)
+
+structure State where
+  cache : Sym.Simp.Cache := {}
+
+initialize homoExt : SolverExtension Sym.Simp.Cache ←
+  registerSolverExtension (return {})
+
+/-- Apply the homomorphism theorems. -/
+def applyHomo (e : Expr) : GoalM Sym.Simp.Result := do
+  let methods := { pre := (← mkRewriter) }
+  -- Reuse cache.
+  let persistentCache ← homoExt.getState
+  homoExt.modifyState fun _ => {} -- Improve uniqueness. This is a minor optimization
+  let (r, s) ← Sym.Simp.SimpM.run (Sym.Simp.simp e) (methods := methods) (s := { persistentCache })
+  homoExt.modifyState fun _ => s.persistentCache
+  return r
+
+/--
+Returns `true` if some theorem marked with `[grind_homo]` is applicable to `e`.
+
+Motivation: we don't want to start the simplifier and fail immediately.
+-/
+def isTarget (e : Expr) : CoreM Bool := do
+  let thms ← getTheorems
+  return !(thms.getMatch e).isEmpty
+
+/--
+Internalization procedure for this module. See `homoExt.setMethods`
+-/
+def internalize (e : Expr) (_ : Option Expr) : GoalM Unit := do
+  unless (← isTarget e) do return ()
+  let .step e₁ h₁ _ ← applyHomo e | return ()
+  let r ← preprocess e₁
+  let h ← mkEqTrans h₁ (← r.getProof)
+  let gen ← getGeneration e
+  Grind.internalize r.expr gen
+  trace[homo] "{e}\n====>\n{r.expr}"
+  pushEq e r.expr h
+
+initialize
+  homoExt.setMethods
+    (internalize := internalize)
+
+end Homomorphism

tests/pkg/homo/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package homo
+@[default_target] lean_lib Homo

tests/pkg/homo/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/homo/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build