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>

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/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/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/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/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