feat: lake: empty build detection & --allow-empty (#13500)

This PR adds a check for empty `lake build` invocations (as an empty
build usually indicates a misconfiguration). Builds with no jobs will
now print "Nothing to build." and invocations of `lake build` with no
default targets configured will produce a warning. This will be promoted
to an error in the future. The warning (and future error) can be
suppressed with the new `--allow-empty` CLI option.

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.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/Data/PPContext.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Data.OpenDecl
+public import Lean.Environment
+public import Lean.MetavarContext
+
+public section
+
+namespace Lean
+
+/-- Saved context for pretty printing. See `Lean.ppExt`. -/
+structure PPContext where
+  env           : Environment
+  mctx          : MetavarContext := {}
+  lctx          : LocalContext := {}
+  opts          : Options := {}
+  currNamespace : Name := Name.anonymous
+  openDecls     : List OpenDecl := []
+
+end Lean

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

@@ -45,15 +45,6 @@ def ContInfoRef : Type := ContInfoRefPointed.type
 instance : Nonempty ContInfoRef :=
   by exact ContInfoRefPointed.property
 
--- Same pattern as `ContInfoRef` above; used so `Context` can carry `DoOps` without
--- depending on `DoElabM`.
-private opaque DoOpsRefPointed : NonemptyType.{0}
-
-def DoOpsRef : Type := DoOpsRefPointed.type
-
-instance : Nonempty DoOpsRef :=
-  by exact DoOpsRefPointed.property
-
 /-- Whether a code block is alive or dead. -/
 inductive CodeLiveness where
   /-- We inferred the code is semantically dead and don't need to elaborate it at all. -/
@@ -99,37 +90,9 @@ structure Context where
   Whether the current `do` element is dead code. `elabDoElem` will emit a warning if not `.alive`.
   -/
   deadCode : CodeLiveness := .alive
-  /-- Pluggable builders for `pure` and `bind` applications. -/
-  ops : DoOpsRef
 
 abbrev DoElabM := ReaderT Context Term.TermElabM
 
-/-- Pluggable builders for the `pure` / `bind` applications emitted by the `do` elaborator. -/
-structure DoOps where
-  /-- Build `pure (α:=α) e : m α`. -/
-  mkPureApp : (α e : Expr) → DoElabM Expr
-  /-- Build `bind (α:=α) (β:=β) e k : m β`. -/
-  mkBindApp : (α β e k : Expr) → DoElabM Expr
-  /--
-  If `e` is syntactically a `pure …` application, return the pure value; otherwise `none`.
-  Used by `DoElemCont.mkBindUnlessPure` to contract `e >>= pure` to `e` and
-  `pure e >>= k` to `let x := e; k x`.
-  -/
-  isPureApp? : Expr → Option Expr
-  deriving Inhabited
-
-unsafe def DoOps.toDoOpsRefImpl (o : DoOps) : DoOpsRef :=
-  unsafeCast o
-
-@[implemented_by DoOps.toDoOpsRefImpl]
-opaque DoOps.toDoOpsRef (o : DoOps) : DoOpsRef
-
-unsafe def DoOpsRef.toDoOpsImpl (r : DoOpsRef) : DoOps :=
-  unsafeCast r
-
-@[implemented_by DoOpsRef.toDoOpsImpl]
-opaque DoOpsRef.toDoOps (r : DoOpsRef) : DoOps
-
 /--
 Whether the continuation of a `do` element is duplicable and if so whether it is just `pure r` for
 the result variable `r`. Saying `nonDuplicable` is always safe; `duplicable` allows for more
@@ -238,7 +201,16 @@ def mkPUnitUnit : DoElabM Expr := do
 
 /-- The expression ``pure (α:=α) e``. -/
 def mkPureApp (α e : Expr) : DoElabM Expr := do
-  (← read).ops.toDoOps.mkPureApp α e
+  let info := (← read).monadInfo
+  if (← read).deadCode matches .deadSyntactically then
+    -- There is no dead syntax here. Just return a fresh metavariable so that we don't
+    -- do the `Term.ensureHasType` check below.
+    return ← mkFreshExprMVar (mkApp info.m α)
+  let α ← Term.ensureHasType (mkSort (mkLevelSucc info.u)) α
+  let e ← Term.ensureHasType α e
+  let instPure ← Term.mkInstMVar (mkApp (mkConst ``Pure [info.u, info.v]) info.m)
+  let instPure ← instantiateMVars instPure
+  return mkApp4 (mkConst ``Pure.pure [info.u, info.v]) info.m instPure α e
 
 /-- Create a `DoElemCont` returning the result using `pure`. -/
 def DoElemCont.mkPure (resultType : Expr) : TermElabM DoElemCont := do
@@ -257,31 +229,13 @@ def ReturnCont.mkPure (resultType : Expr) : TermElabM ReturnCont := do
 
 /-- The expression ``Bind.bind (α:=α) (β:=β) e k``. -/
 def mkBindApp (α β e k : Expr) : DoElabM Expr := do
-  (← read).ops.toDoOps.mkBindApp α β e k
-
-/-- `DoOps` emitting `Pure.pure` / `Bind.bind`. -/
-def DoOps.default : DoOps where
-  mkPureApp α e := do
-    let info := (← read).monadInfo
-    if (← read).deadCode matches .deadSyntactically then
-      -- There is no dead syntax here. Just return a fresh metavariable so that we don't
-      -- do the `Term.ensureHasType` check below.
-      return ← mkFreshExprMVar (mkApp info.m α)
-    let α ← Term.ensureHasType (mkSort (mkLevelSucc info.u)) α
-    let e ← Term.ensureHasType α e
-    let instPure ← Term.mkInstMVar (mkApp (mkConst ``Pure [info.u, info.v]) info.m)
-    let instPure ← instantiateMVars instPure
-    return mkApp4 (mkConst ``Pure.pure [info.u, info.v]) info.m instPure α e
-  mkBindApp α β e k := do
-    let info := (← read).monadInfo
-    let α ← Term.ensureHasType (mkSort (mkLevelSucc info.u)) α
-    let mα := mkApp info.m α
-    let e ← Term.ensureHasType mα e
-    let k ← Term.ensureHasType (← mkArrow α (mkApp info.m β)) k
-    let instBind ← Term.mkInstMVar (mkApp (mkConst ``Bind [info.u, info.v]) info.m)
-    return mkApp6 (mkConst ``Bind.bind [info.u, info.v]) info.m instBind α β e k
-  isPureApp? e :=
-    if e.isAppOfArity ``Pure.pure 4 then some (e.getArg! 3) else none
+  let info := (← read).monadInfo
+  let α ← Term.ensureHasType (mkSort (mkLevelSucc info.u)) α
+  let mα := mkApp info.m α
+  let e ← Term.ensureHasType mα e
+  let k ← Term.ensureHasType (← mkArrow α (mkApp info.m β)) k
+  let instBind ← Term.mkInstMVar (mkApp (mkConst ``Bind [info.u, info.v]) info.m)
+  return mkApp6 (mkConst ``Bind.bind [info.u, info.v]) info.m instBind α β e k
 
 /-- Register the given name as that of a `mut` variable. -/
 def declareMutVar (x : Ident) (k : DoElabM α) : DoElabM α := do
@@ -480,19 +434,18 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
-    let ops := (← read).ops.toDoOps
     -- First try to contract `e >>= pure` into `e`.
     -- Reason: for `pure e >>= pure`, we want to get `pure e` and not `have xFVar := e; pure xFVar`.
-    if let some pureArg := ops.isPureApp? body' then
-      if pureArg == xFVar then
-        let body'' ← mkPureApp eResultTy xFVar
-        if ← withNewMCtxDepth do isDefEq body' body'' then
-          return e
+    if body'.isAppOfArity ``Pure.pure 4 && body'.getArg! 3 == xFVar then
+      let body'' ← mkPureApp eResultTy xFVar
+      if ← withNewMCtxDepth do isDefEq body' body'' then
+        return e
 
     -- Now test whether we can contract `pure e >>= k` into `have xFVar := e; k xFVar`. We zeta `xFVar` when
     -- `e` is duplicable; we don't look at `k` to see whether it is used at most once.
     let e' := e.consumeMData
-    if let some eRes := ops.isPureApp? e' then
+    if e'.isAppOfArity ``Pure.pure 4 then
+      let eRes := e'.getArg! 3
       let e' ← mkPureApp eResultTy eRes
       let (isPure, isDuplicable) ← withNewMCtxDepth do
         let isPure ← isDefEq e e'
@@ -730,12 +683,11 @@ where
     return ({ m, u, v }, resultType)
 
 /-- Create the `Context` for `do` elaboration from the given expected type of a `do` block. -/
-def mkContext (expectedType? : Option Expr) (ops : DoOps := .default) : TermElabM Context := do
+def mkContext (expectedType? : Option Expr) : TermElabM Context := do
   let (mi, resultType) ← extractMonadInfo expectedType?
   let returnCont ← ReturnCont.mkPure resultType
   let contInfo := ContInfo.toContInfoRef { returnCont }
-  return { monadInfo := mi, doBlockResultType := resultType, contInfo,
-           ops := ops.toDoOpsRef }
+  return { monadInfo := mi, doBlockResultType := resultType, contInfo }
 
 section NestedActions
 
@@ -951,11 +903,11 @@ def elabNestedAction : Term.TermElab := fun stx _ty? => do
   let `(← $_rhs) := stx | throwUnsupportedSyntax
   throwErrorAt stx "Nested action `{stx}` must be nested inside a `do` expression."
 
-/-- Elaborate `doSeq` using `ops` for pure/bind construction. -/
-def elabDoWith (ops : DoOps) (doSeq : TSyntax ``doSeq)
-    (expectedType? : Option Expr) : TermElabM Expr := do
+-- @[builtin_term_elab «do»] -- once the legacy `do` elaborator has been phased out
+def elabDo : Term.TermElab := fun e expectedType? => do
+  let `(do $doSeq) := e | throwError "unexpected `do` block syntax{indentD e}"
   Term.tryPostponeIfNoneOrMVar expectedType?
-  let ctx ← mkContext expectedType? (ops := ops)
+  let ctx ← mkContext expectedType?
   let cont ← DoElemCont.mkPure ctx.doBlockResultType
   let res ← elabDoSeq doSeq cont |>.run ctx
   -- Synthesizing default instances here is harmful for expressions such as
@@ -968,8 +920,3 @@ def elabDoWith (ops : DoOps) (doSeq : TSyntax ``doSeq)
   -- Term.synthesizeSyntheticMVarsUsingDefault
   trace[Elab.do] "{← instantiateMVars res}"
   pure res
-
--- @[builtin_term_elab «do»] -- once the legacy `do` elaborator has been phased out
-def elabDo : Term.TermElab := fun e expectedType? => do
-  let `(do $doSeq) := e | throwError "unexpected `do` block syntax{indentD e}"
-  elabDoWith .default doSeq expectedType?

src/Lean/Elab/InfoTree/Main.lean

@@ -216,11 +216,21 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"[FieldRedecl] @ {formatStxRange ctx info.stx}"
 
+def DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) : IO (Option String) := do
+  match info.mkDocString? with
+  | none => return none
+  | some act =>
+    try
+      act ppCtx
+    catch ex =>
+      return s!"[Error: {ex.toString}]"
+
 def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
   let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
+  let docString? ← info.docString? (ctx.toPPContext info.lctx)
   return f!"[DelabTerm] @ {← TermInfo.format ctx info.toTermInfo}\n\
     Location: {loc}\n\
-    Docstring: {repr info.docString?}\n\
+    Docstring: {repr docString?}\n\
     Explicit: {info.explicit}"
 
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=

src/Lean/Elab/InfoTree/Types.lean

@@ -9,6 +9,7 @@ module
 prelude
 public import Lean.Data.DeclarationRange
 public import Lean.Data.OpenDecl
+public import Lean.Data.PPContext
 public import Lean.MetavarContext
 public import Lean.Environment
 public import Lean.Widget.Types
@@ -208,8 +209,10 @@ regular delaboration settings. Additionally, omissions come with a reason for om
 structure DelabTermInfo extends TermInfo where
   /-- A source position to use for "go to definition", to override the default. -/
   location? : Option DeclarationLocation := none
-  /-- Text to use to override the docstring. -/
-  docString? : Option String := none
+  /-- Text to use to override the docstring. The string may be dynamic text. It is an `IO` action
+  so that it can be computed only when it is used. The action receives a `PPContext` so that the
+  action does not need to create a closure with the meta state. -/
+  mkDocString? : Option (PPContext → IO String) := none
   /-- Whether to use explicit mode when pretty printing the term on hover. -/
   explicit : Bool := true
 

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/Lean/Meta/Basic.lean

@@ -2223,10 +2223,14 @@ def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnot
     | _ => throwError "invalid `instantiateForallWithParams`, too many parameters{indentExpr e}"
   return (res, e)
 
+def getPPContext : MetaM PPContext := do
+  return { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptions),
+           currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls) }
+
 /-- Pretty-print the given expression. -/
 def ppExprWithInfos (e : Expr) : MetaM FormatWithInfos := do
-  let ctxCore  ← readThe Core.Context
-  Lean.ppExprWithInfos { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptions), currNamespace := ctxCore.currNamespace, openDecls := ctxCore.openDecls } e
+  let ctx ← getPPContext
+  Lean.ppExprWithInfos ctx e
 
 /-- Pretty-print the given expression. -/
 def ppExpr (e : Expr) : MetaM Format := (·.fmt) <$> ppExprWithInfos e

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -48,6 +48,9 @@ structure Context where
   subExpr        : SubExpr
   /-- Current recursion depth during delaboration. Used by the `pp.deepTerms false` option. -/
   depth          : Nat := 0
+  /-- Initial state of `LocalContext.numIndices`, to keep track of which variables were introduced
+  during delaboration. -/
+  lctxInitIndices : Nat
 
 structure State where
   /-- The number of `delab` steps so far. Used by `pp.maxSteps` to stop delaboration. -/
@@ -220,12 +223,21 @@ where
     stx := stx
   }
 
+/--
+Adds `DelabTermInfo` at the given position.
+
+Either `docString?` or `mkDocString?` can be provided. The `docString?` field is a convenient
+interface for `mkDocString?`.
+-/
 def addDelabTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
-    (location? : Option DeclarationLocation := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
+    (location? : Option DeclarationLocation := none)
+    (docString? : Option String := none)
+    (mkDocString? : Option (PPContext → IO String) := none)
+    (explicit : Bool := true) : DelabM Unit := do
   let info := Info.ofDelabTermInfo {
     toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := isBinder)
     location?  := location?
-    docString? := docString?
+    mkDocString? := mkDocString? <|> docString?.map (fun _ => pure ·)
     explicit   := explicit
   }
   modify fun s => { s with infos := s.infos.insert pos info }
@@ -515,7 +527,8 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM
             currNamespace := (← getCurrNamespace)
             openDecls := (← getOpenDecls)
             subExpr := SubExpr.mkRoot e
-            inPattern := opts.getInPattern }
+            inPattern := opts.getInPattern
+            lctxInitIndices := (← getLCtx).numIndices }
           |>.run { : Delaborator.State })
         (fun _ => unreachable!)
     return (stx, infos)

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.PrettyPrinter.Delaborator.Basic
+public import Lean.PrettyPrinter.Delaborator.Metavariable
 public import Lean.Meta.CoeAttr
 public import Lean.Meta.Structure
 public import Lean.PrettyPrinter.Formatter
@@ -60,29 +61,14 @@ def delabBVar : Delab := do
   let Expr.bvar idx ← getExpr | unreachable!
   pure $ mkIdent $ Name.mkSimple $ "#" ++ toString idx
 
-def delabMVarAux (m : MVarId) : DelabM Term := do
-  let mkMVarPlaceholder : DelabM Term := `(?_)
-  let mkMVar (n : Name) : DelabM Term := `(?$(mkIdent n))
-  withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
-    if ← getPPOption getPPMVars then
-      if let some decl ← m.findDecl? then
-        match decl.userName with
-        | .anonymous =>
-          if ← getPPOption getPPMVarsAnonymous then
-            mkMVar <| Name.num `m (decl.index + 1)
-          else
-            mkMVarPlaceholder
-        | n => mkMVar n
-      else
-        -- Undefined mvar, use internal name
-        mkMVar <| m.name.replacePrefix `_uniq `_mvar
-    else
-      mkMVarPlaceholder
-
 @[builtin_delab mvar]
 def delabMVar : Delab := do
-  let Expr.mvar n ← getExpr | unreachable!
-  delabMVarAux n
+  let Expr.mvar mvarId ← getExpr | unreachable!
+  withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
+    let stx ← annotateCurPos =<< delabMVarAux mvarId
+    let descr ← mkDescribeMVar mvarId
+    addDelabTermInfo (← getPos) stx (← getExpr) (mkDocString? := some descr) (explicit := true)
+    return stx
 
 @[builtin_delab sort]
 def delabSort : Delab := do
@@ -593,10 +579,17 @@ def delabDelayedAssignedMVar : Delab := whenNotPPOption getPPMVarsDelayed do
   let .mvar mvarId := (← getExpr).getAppFn | failure
   let some decl ← getDelayedMVarAssignment? mvarId | failure
   withOverApp decl.fvars.size do
-    let args := (← getExpr).getAppArgs
-    -- Only delaborate using decl.mvarIdPending if the delayed mvar is applied to fvars
-    guard <| args.all Expr.isFVar
-    delabMVarAux decl.mvarIdPending
+    guard <| ← checkDelayedMVarAssignment (← getExpr) decl
+    let mvarIdPending ← getDelayedMVarIdPending decl.mvarIdPending
+    let descr ← mkDescribeMVar mvarIdPending (fromDelayed := true)
+    withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
+      -- Delaborate the whole application as if it were a single metavariable.
+      -- Hovering will show the underlying delayed assignment expression, and the type
+      -- will be the type of the application itself (which is valid in the current local context,
+      -- unlike the type of `mvarIdPending`).
+      let stx ← annotateCurPos =<< delabMVarAux mvarIdPending
+      addDelabTermInfo (← getPos) stx (← getExpr) (explicit := true) (mkDocString? := descr)
+      return stx
 
 private partial def collectStructFields
     (structName : Name) (levels : List Level) (params : Array Expr)

src/Lean/PrettyPrinter/Delaborator/Metavariable.lean

@@ -0,0 +1,205 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+module
+
+prelude
+public import Lean.PrettyPrinter.Delaborator.Basic
+import all Lean.Elab.ErrorUtils
+
+public section
+
+namespace Lean.PrettyPrinter.Delaborator
+open Lean.Meta
+
+/-!
+# Utilities for pretty printing metavariables and generating dynamic docstrings
+-/
+
+private def delabMVarAuxAux {α} (m : MVarId)
+    (mkMVarPlaceholder : MetaM α) (mkMVar : Name → MetaM α) (mkMVarDead : Name → MetaM α)
+    (ppMVars : Bool)
+    (ppMVarsAnonymous : Bool) :
+    MetaM α := do
+  if ppMVars then
+    if let some decl ← m.findDecl? then
+      match decl.userName with
+      | .anonymous =>
+        if ppMVarsAnonymous then
+          mkMVar <| Name.num `m (decl.index + 1)
+        else
+          mkMVarPlaceholder
+      | n =>
+        if some m == (← getMCtx).findUserName? n then
+          mkMVar n
+        else
+          mkMVarDead n
+    else
+      -- Undefined mvar, use internal name
+      mkMVar <| m.name.replacePrefix `_uniq `_mvar
+  else
+    mkMVarPlaceholder
+
+/--
+Constructs a `?m` term using the name of `m` or its index. Does not add terminfo.
+The metavariable does not need to be type correct in the current local context.
+-/
+def delabMVarAux (m : MVarId) : DelabM Term := do
+  delabMVarAuxAux m `(?_) (fun n => `(?$(mkIdent n)))
+    (fun n =>
+      let n' := addMacroScope (`_delabMVar ++ m.name) n reservedMacroScope
+      `(?$(mkIdent n')))
+    (ppMVars := ← getPPOption getPPMVars)
+    (ppMVarsAnonymous := ← getPPOption getPPMVarsAnonymous)
+
+/-- String version of `delabMVarAux`, for use in dynamic docstrings. -/
+private def delabMVarAsStr (m : MVarId) : MetaM String := do
+  delabMVarAuxAux m (pure "?_") (fun n : Name => pure <| "?" ++ n.toString)
+    (fun n => pure <| "?" ++ n.toString ++ " (unreachable)")
+    (ppMVars := getPPMVars (← getOptions))
+    (ppMVarsAnonymous := getPPMVarsAnonymous (← getOptions))
+
+/--
+Approximate check that the application `?m a₁ … aₙ` of the delayed assignment metavariable `?m`
+can be pretty printed using the pending metavariable.
+
+Heuristic: we assume the ldecl arguments are correct, and for the cdecls we check that they are
+distinct fvars
+-/
+def checkDelayedMVarAssignment (e : Expr) (decl : DelayedMetavarAssignment) : MetaM Bool := do
+  unless e.getAppNumArgs == decl.fvars.size do
+    return false
+  let some mdecl ← decl.mvarIdPending.findDecl? | return false
+  let mut seenFVars : FVarIdHashSet := {}
+  for fvar in decl.fvars, arg in e.getAppArgs do
+    let fvarId := fvar.fvarId!
+    let some ldecl := mdecl.lctx.find? fvarId | return false
+    unless ldecl.hasValue do
+      let .fvar argFVarId := arg | return false
+      if seenFVars.contains argFVarId then
+        return false
+      seenFVars := seenFVars.insert argFVarId
+  return true
+
+/--
+Follows a chain of delayed assignments to find the pending metavariable.
+-/
+partial def getDelayedMVarIdPending (mvarIdPending : MVarId) : MetaM MVarId := do
+  let some e ← getExprMVarAssignment? mvarIdPending | return mvarIdPending
+  unless e.getAppFn'.isMVar do return mvarIdPending
+  let e := (← instantiateMVars e).consumeMData
+  if let .mvar mvarId := e then
+    return mvarId
+  let .mvar mvarId := e.getAppFn' | return mvarIdPending
+  if let some decl ← getDelayedMVarAssignment? mvarId then
+    unless ← checkDelayedMVarAssignment e decl do return mvarIdPending
+    getDelayedMVarIdPending decl.mvarIdPending
+  else
+    return mvarIdPending
+
+private def describeMVar (mvarId : MVarId) (lctxInitIndices : Nat) (fromDelayed : Bool := false) : MetaM String := do
+  let delayedExpl :=
+    "Substitution is delayed until the metavariable's value contains no metavariables, \
+     since all occurrences of the variables from its local context will need to be \
+     replaced with expressions that are valid in the current context."
+  let some decl ← mvarId.findDecl? | return "[Error: This metavariable is not present in the metavariable context. Please report this issue.]"
+  let mut msg := ""
+  if let some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
+    let mvarIdPending' ← getDelayedMVarIdPending mvarIdPending
+    if let some declPending' ← mvarIdPending'.findDecl? then
+      msg := s!"Part of the encoding of the *delayed assignment* mechanism. \
+        Represents the metavariable {← wrap <$> delabMVarAsStr mvarIdPending'}, \
+        which has additional local context variables. \
+        {delayedExpl}"
+      if let some e ← getExprMVarAssignment? mvarIdPending' then
+        msg := msg ++ (← collectAwaiting e)
+      msg := msg ++ (← extraLCtxVars declPending')
+    else
+      msg := "[Error: This delayed assignment refers to a metavariable not present in the metavariable context. Please report this issue.]"
+    return msg
+  else
+    match decl.kind with
+    | .natural =>
+      msg := "A metavariable representing an expression that should be solved for \
+        by unification during the elaboration process. \
+        They are created during elaboration as placeholders for implicit arguments \
+        and by `_` placeholder syntax."
+    | .synthetic =>
+      msg := "A metavariable representing a typeclass instance whose synthesis is still pending. \
+        They can be solved for by unification during the elaboration process, \
+        but the inferred expression and the synthesized instance must be definitionally equal."
+    | .syntheticOpaque =>
+      msg := "A metavariable representing a tactic goal or an expression whose elaboration is still pending. \
+        They usually act like constants until they are completely solved for. \
+        They can be created using `?_` and `?n` synthetic placeholder syntax."
+  unless decl.userName.isAnonymous || some mvarId == (← getMCtx).findUserName? decl.userName do
+    msg := msg ++ "\n\nThis metavariable has a name but it is unreachable."
+  if let some e ← getExprMVarAssignment? mvarId then
+    if !fromDelayed then
+      msg := msg ++ "\n\nThis metavariable has been assigned."
+    else
+      msg := msg ++ "\n\nThis metavariable has been assigned, but it appears here via a *delayed assignment*. " ++ delayedExpl
+      msg := msg ++ (← collectAwaiting e)
+  else if !(← mvarId.isAssignable) then
+    msg := msg ++ "\n\nThis metavariable cannot be assigned due to the current metavariable context depth."
+  else if fromDelayed then
+    msg := msg ++ "\n\nThis metavariable appears here via a *delayed assignment*. " ++ delayedExpl
+  if fromDelayed && !decl.lctx.isSubPrefixOf (← getLCtx) then
+    msg := msg ++ (← extraLCtxVars decl)
+  else
+    msg := msg ++ (← absentLCtxVars decl)
+  return msg
+where
+  wrap (n : String) := s!"`{n}`"
+  namesToString (ns : List Name) : String :=
+    String.intercalate ", " <| ns.map fun n => wrap <|
+      if n.hasMacroScopes then
+        n.eraseMacroScopes.toString ++ " (unreachable)"
+      else
+        n.toString
+  extraLCtxVars (mdecl : MetavarDecl) : MetaM String := do
+    let lctx ← getLCtx
+    let ns := mdecl.lctx.foldr (init := []) fun decl ns =>
+      if lctx.contains decl.fvarId then ns else decl.userName :: ns
+    if ns.isEmpty then
+      return ""
+    else
+      return s!"\n\nAdditional {ns.length.plural "variable"} in this metavariable's local context: " ++ namesToString ns
+  absentLCtxVars (mdecl : MetavarDecl) : MetaM String := do
+    let lctx ← getLCtx
+    let lctxInitIndices := lctxInitIndices
+    let ns := lctx.foldr (init := []) fun decl ns =>
+      if decl.index ≥ lctxInitIndices || mdecl.lctx.contains decl.fvarId then ns else decl.userName :: ns
+    if ns.isEmpty then
+      return ""
+    else
+      return s!"\n\n{ns.length.plural "Variable"} absent from this metavariable's local context: " ++ namesToString ns
+  collectAwaiting (e : Expr) : MetaM String := do
+    -- Collect metavariables to diagnose why it is pending.
+    let mut awaitingMVars ← getMVarsNoDelayed e
+    -- Prefer reporting just the metavariables that refer to free variables not in the current context.
+    let lctx ← getLCtx
+    let awaitingMVars' ← awaitingMVars.filterM fun mvar => do
+      let mdecl ← mvar.getDecl
+      return !mdecl.lctx.isSubPrefixOf lctx
+    unless awaitingMVars'.isEmpty do
+      awaitingMVars := awaitingMVars'
+    if awaitingMVars.isEmpty then
+      return ""
+    else
+      let awaitingStrs ← awaitingMVars.mapM (wrap <$> delabMVarAsStr ·)
+      return s!" Substitution is awaiting assignment of the following {awaitingStrs.size.plural "metavariable"}: "
+        ++ String.intercalate ", " awaitingStrs.toList
+
+/--
+Creates an action that creates a description of the metavariable and its status in Markdown format,
+for use in the docstring in `DelabTermInfo`.
+-/
+def mkDescribeMVar (mvarId : MVarId) (fromDelayed : Bool := false) :
+    DelabM (PPContext → IO String) := do
+  let lctxInitIndices := (← read).lctxInitIndices
+  return fun ppCtx => ppCtx.runMetaM do describeMVar mvarId lctxInitIndices (fromDelayed := fromDelayed)
+
+end Lean.PrettyPrinter.Delaborator

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -72,12 +72,14 @@ where
   maybeWithoutTopLevelHighlight : Bool → CodeWithInfos → CodeWithInfos
     | true, .tag _ tt => tt
     | _,    tt        => tt
-  ppExprForPopup (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
-    let mut e := e
+  ppExprForPopup (e : Expr) (explicit : Bool) : MetaM CodeWithInfos := do
     -- When hovering over a metavariable, we want to see its value, even if `pp.instantiateMVars` is false.
-    if explicit && e.isMVar then
-      if let some e' ← getExprMVarAssignment? e.mvarId! then
-        e := e'
+    if explicit then
+      if let .mvar mvarId := e then
+        if let some e' ← getExprMVarAssignment? mvarId then
+          return ← ppExprForPopupAux e' false
+    ppExprForPopupAux e explicit
+  ppExprForPopupAux (e : Expr) (explicit : Bool) : MetaM CodeWithInfos := do
     -- When `explicit` is false, keep the top-level tag so that users can also see the explicit version of the term on an additional hover.
     maybeWithoutTopLevelHighlight explicit <$> ppExprTagged e do
       if explicit then

src/Lean/Server/InfoUtils.lean

@@ -328,11 +328,14 @@ def Info.type? (i : Info) : MetaM (Option Expr) :=
 def Info.docString? (i : Info) : MetaM (Option String) := do
   let env ← getEnv
   match i with
-  | .ofDelabTermInfo { docString? := some s, .. } => return s
-  | .ofTermInfo ti
-  | .ofDelabTermInfo ti =>
+  | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
       return (← findDocString? env n)
+  | .ofDelabTermInfo ti =>
+    if let some doc ← ti.docString? (← Meta.getPPContext) then
+      return doc
+    else if let some n := ti.expr.constName? then
+      return (← findDocString? env n)
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then

src/Lean/Util/PPExt.lean

@@ -29,14 +29,6 @@ register_builtin_option pp.rawOnError : Bool := {
   descr    := "(pretty printer) fallback to 'raw' printer when pretty printer fails"
 }
 
-structure PPContext where
-  env           : Environment
-  mctx          : MetavarContext := {}
-  lctx          : LocalContext := {}
-  opts          : Options := {}
-  currNamespace : Name := Name.anonymous
-  openDecls     : List OpenDecl := []
-
 abbrev PrettyPrinter.InfoPerPos := Std.TreeMap Nat Elab.Info
 /-- A format tree with `Elab.Info` annotations.
 Each `.tag n _` node is annotated with `infos[n]`.

src/lake/Lake/Build/Run.lean

@@ -284,11 +284,14 @@ def reportResult (cfg : BuildConfig) (out : IO.FS.Stream) (result : MonitorResul
   if result.failures.isEmpty then
     if cfg.showProgress && cfg.showSuccess then
       let numJobs := result.numJobs
-      let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
-      if cfg.noBuild then
-        print! out s!"All targets up-to-date ({jobs}).\n"
+      if numJobs == 0 then
+        print! out "Nothing to build.\n"
       else
-        print! out s!"Build completed successfully ({jobs}).\n"
+        let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
+        if cfg.noBuild then
+          print! out s!"All targets up-to-date ({jobs}).\n"
+        else
+          print! out s!"Build completed successfully ({jobs}).\n"
   else
     print! out "Some required targets logged failures:\n"
     result.failures.forM (print! out s!"- {·}\n")

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
@@ -55,6 +55,7 @@ BASIC OPTIONS:
   --packages=file       JSON file of package entries that override the manifest
   --reconfigure, -R     elaborate configuration files instead of using OLeans
   --keep-toolchain      do not update toolchain on workspace update
+  --allow-empty         accept bare builds with no default targets configured
   --no-build            exit immediately if a build target is not up-to-date
   --no-cache            build packages locally; do not download build caches
   --try-cache           attempt to download build caches for supported packages
@@ -242,17 +243,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
@@ -55,6 +56,7 @@ public structure LakeOptions where
   reconfigure : Bool := false
   oldMode : Bool := false
   trustHash : Bool := true
+  allowEmpty : Bool := false
   noBuild : Bool := false
   noCache : Option Bool := none
   failLv : LogLevel := .error
@@ -72,6 +74,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
@@ -241,6 +248,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
 | "--text"        => modifyThe LakeOptions ({· with outFormat := .text})
 | "--json"        => modifyThe LakeOptions ({· with outFormat := .json})
+| "--allow-empty" => modifyThe LakeOptions ({· with allowEmpty := true})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
 | "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
 | "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
@@ -302,12 +310,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})
@@ -827,6 +847,12 @@ protected def build : CliM PUnit := do
   let ws ← loadWorkspace config
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
+  if specs.isEmpty && !opts.allowEmpty then
+    logWarning "no targets specified and no default targets configured\
+      \n  Note: This will be an error in a future version of Lake.\
+      \n  Hint: This warning (or error) can be suppressed with '--allow-empty'."
+    if opts.failLv ≤ .warning then
+      exit 1
   specs.forM fun spec =>
     unless spec.buildable do
       throw <| .invalidBuildTarget spec.info.key.toSimpleString
@@ -945,18 +971,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/474.lean.out.expected

@@ -4,5 +4,5 @@ fun y_1 => y.add y_1
 fun y => Nat.add FREE y
 fun (y : Nat) => Nat.add y y
 Nat.add ?m y
-Nat.add (?m #0) #0
+Nat.add ?m #0
 fun y => (y.add y).add y

tests/elab/doNotationPluggableOps.lean

@@ -1,217 +0,0 @@
-import Lean
-
-/-!
-Tests for the pluggable pure/bind builders in the `do` elaborator (`DoOps`, `elabDoWith`).
-
-We define a surface `ido` notation that reuses the full `do` elaborator via `elabDoWith`
-but emits `IxMonad.pure` / `IxMonad.bind` instead of `Pure.pure` / `Bind.bind`.
-
-`IxMonad` is the canonical Atkey parameterised monad (`m : ι → ι → Type u → Type v` with
-`pure : α → m i i α` and `bind : m i j α → (α → m j k β) → m i k β`); the shape is
-documented in `Control.Monad.Indexed` on Hackage and the PureScript `indexed-monad`
-package.
-
-The control-stack features of `do` (`mut`, `return`, `break`, `continue`, `for`) remain
-hard-coded to `Monad` and are therefore off-limits for `ido`. The `ido` programs below
-avoid them.
--/
-
-open Lean Lean.Parser Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term
-
-set_option backward.do.legacy false
-
-/-! ## Indexed monad and a concrete instance -/
-
-class IxMonad (m : ι → ι → Type u → Type v) where
-  pure : α → m i i α
-  bind : m i j α → (α → m j k β) → m i k β
-
-/-- Atkey-style indexed state: `IState i o α = i → α × o`. -/
-abbrev IState (i o α : Type) : Type := i → α × o
-
-instance : IxMonad IState where
-  pure a := fun i => (a, i)
-  bind p f := fun i => let (a, j) := p i; f a j
-
-/-! Helpers that keep the state type fixed at `Nat` for the common examples. -/
-
-def getN : IState Nat Nat Nat := fun s => (s, s)
-def putN (n : Nat) : IState Nat Nat Unit := fun _ => ((), n)
-def modifyN (f : Nat → Nat) : IState Nat Nat Unit := fun i => ((), f i)
-
-/-! ## Pluggable ops emitting `IxMonad.pure` / `IxMonad.bind` -/
-
-def ixOps : DoOps where
-  mkPureApp α e := do
-    let info := (← read).monadInfo
-    let mα := mkApp info.m α
-    let eStx ← Term.exprToSyntax e
-    let stx ← `(IxMonad.pure $eStx)
-    Term.elabTermEnsuringType stx mα
-  mkBindApp α β e k := do
-    let info := (← read).monadInfo
-    let mβ := mkApp info.m β
-    let eStx ← Term.exprToSyntax e
-    let kStx ← Term.exprToSyntax k
-    let stx ← `(IxMonad.bind $eStx $kStx)
-    Term.elabTermEnsuringType stx mβ
-  isPureApp? e :=
-    -- `@IxMonad.pure ι m inst α i e` — 6 args.
-    if e.isAppOfArity ``IxMonad.pure 6 then some (e.getArg! 5) else none
-
-/-! ## `ido` surface syntax -/
-
-syntax (name := idoKind) "ido " doSeq : term
-
-@[term_elab idoKind] def elabIDo : Term.TermElab := fun stx et? => do
-  let `(ido $doSeq) := stx | throwUnsupportedSyntax
-  elabDoWith ixOps doSeq et?
-
-/-! ## Example programs
-
-Each example pairs `#guard_msgs` with `#eval` (or `#check`) to lock behaviour in.
-Most keep state type fixed at `Nat`; a couple at the end explore index-preserving
-variants with different state types. -/
-
-/-! ### 1. Bare pure -/
-
-/-- info: (42, 10) -/
-#guard_msgs in
-#eval (ido IxMonad.pure 42 : IState Nat Nat Nat) 10
-
-/-! ### 2. Monadic `let ← ` -/
-
-/-- info: (11, 10) -/
-#guard_msgs in
-#eval (ido do
-  let x ← getN
-  IxMonad.pure (x + 1) : IState Nat Nat Nat) 10
-
-/-! ### 3. Plain `let :=` -/
-
-/-- info: (20, 10) -/
-#guard_msgs in
-#eval (ido do
-  let x := 10
-  let y ← getN
-  IxMonad.pure (x + y) : IState Nat Nat Nat) 10
-
-/-! ### 4. Sequential unit-typed element -/
-
-/-- info: (11, 11) -/
-#guard_msgs in
-#eval (ido do
-  modifyN (· + 1)
-  getN : IState Nat Nat Nat) 10
-
-/-! ### 5. Multi-step chain -/
-
-/-- info: ((10, 11), 11) -/
-#guard_msgs in
-#eval (ido do
-  let a ← getN
-  modifyN (· + 1)
-  let b ← getN
-  IxMonad.pure (a, b) : IState Nat Nat (Nat × Nat)) 10
-
-/-! ### 6. Nested `(← …)` in pure context -/
-
-/-- info: (11, 10) -/
-#guard_msgs in
-#eval (ido IxMonad.pure ((← getN) + 1) : IState Nat Nat Nat) 10
-
-/-! ### 7. Nested `(← …)` appearing twice in one expression -/
-
-/-- info: (20, 10) -/
-#guard_msgs in
-#eval (ido IxMonad.pure ((← getN) + (← getN)) : IState Nat Nat Nat) 10
-
-/-! ### 8. `if/then/else` with do branches -/
-
-/-- info: (5, 5) -/
-#guard_msgs in
-#eval (ido do
-  let x ← getN
-  if x > 0 then IxMonad.pure x else IxMonad.pure 0 : IState Nat Nat Nat) 5
-
-/-- info: (0, 0) -/
-#guard_msgs in
-#eval (ido do
-  let x ← getN
-  if x > 0 then IxMonad.pure x else IxMonad.pure 0 : IState Nat Nat Nat) 0
-
-/-! ### 9. `if` with a lifted action in the condition -/
-
-/-- info: ((), 4) -/
-#guard_msgs in
-#eval (ido do
-  if (← getN) > 0 then modifyN (· - 1) else IxMonad.pure () : IState Nat Nat Unit) 5
-
-/-- info: ((), 0) -/
-#guard_msgs in
-#eval (ido do
-  if (← getN) > 0 then modifyN (· - 1) else IxMonad.pure () : IState Nat Nat Unit) 0
-
-/-! ### 10. `match` dispatching into do blocks -/
-
-/-- info: (100, 7) -/
-#guard_msgs in
-#eval (ido do
-  match (← getN) with
-  | 0 => IxMonad.pure 0
-  | _ => IxMonad.pure 100 : IState Nat Nat Nat) 7
-
-/-! ### 11. Pattern `let` -/
-
-/-- info: (3, 0) -/
-#guard_msgs in
-#eval (ido do
-  let (a, b) ← IxMonad.pure (1, 2)
-  IxMonad.pure (a + b) : IState Nat Nat Nat) 0
-
-/-! ### 12. Nested `ido` inside `ido` -/
-
-/-- info: (42, 0) -/
-#guard_msgs in
-#eval (ido do
-  let y ← (ido IxMonad.pure 42 : IState Nat Nat Nat)
-  IxMonad.pure y : IState Nat Nat Nat) 0
-
-/-! ### 13. `ido` composing with ordinary `do` -/
-
-/-- info: 84 -/
-#guard_msgs in
-#eval Id.run do
-  let (n, _) := (ido IxMonad.pure 42 : IState Nat Nat Nat) 0
-  pure (n * 2)
-
-/-! ### 14. `pure e >>= pure` peephole — confirms the generated term has no redundant
-         `IxMonad.bind`.
-
-The equation `(ido do let x ← IxMonad.pure 17; IxMonad.pure x) = IxMonad.pure 17` holds
-definitionally only if the peephole in `mkBindUnlessPure` fired and contracted the bind
-away, emitting a bare `IxMonad.pure 17`. If the peephole failed, the result would be
-`IxMonad.bind (IxMonad.pure 17) IxMonad.pure`, which is not definitionally equal to
-`IxMonad.pure 17` because `IxMonad` is a plain `class` without beta-reduction laws. -/
-
-example : (ido do
-    let x ← IxMonad.pure 17
-    IxMonad.pure x : IState Nat Nat Nat) = IxMonad.pure 17 := rfl
-
-/-! ### 15. Deeper chains of binds -/
-
-/-- info: (6, 10) -/
-#guard_msgs in
-#eval (ido do
-  let a ← IxMonad.pure 1
-  let b ← IxMonad.pure 2
-  let c ← IxMonad.pure 3
-  IxMonad.pure (a + b + c) : IState Nat Nat Nat) 10
-
-/-! ### 16. Index-preserving monad with a different fixed state type -/
-
-/-- info: ("hi there", "hi") -/
-#guard_msgs in
-#eval (ido do
-  let s ← (fun (σ : String) => (σ, σ) : IState String String String)
-  IxMonad.pure (s ++ " there") : IState String String String) "hi"

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/elab/forInListSpecUnivPoly.lean.out.expected

@@ -621,57 +621,61 @@
         wp⟦pure (ForInStep.yield r✝)⟧
           (fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv),
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝),
         (fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv).snd)
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝).snd)
 [Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦pure PUnit.unit⟧
       (fun a =>
         wp⟦pure (ForInStep.yield r✝)⟧
           (fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv),
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝),
         (fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv).snd)
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝).snd)
 [Elab.Tactic.Do.spec] discharge? (wp⟦pure PUnit.unit⟧
         (fun a =>
           wp⟦pure (ForInStep.yield r✝)⟧
             (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv),
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝),
           (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv).snd)).down
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝).snd)).down
 [Elab.Tactic.Do.spec] pure Prop: (wp⟦pure PUnit.unit⟧
         (fun a =>
           wp⟦pure (ForInStep.yield r✝)⟧
             (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv),
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝),
           (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv).snd)).down
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝).snd)).down
 [Elab.Tactic.Do.spec] Candidates for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
 [Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
 [Elab.Tactic.Do.spec] Specs for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
@@ -679,88 +683,94 @@
           wp⟦pure (ForInStep.yield r✝)⟧
             (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv),
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝),
           (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv).snd).fst
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝).snd).fst
       PUnit.unit
 [Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun a =>
           wp⟦pure (ForInStep.yield r✝)⟧
             (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv),
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝),
           (fun r =>
               match r with
-              | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+              | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
               | ForInStep.done b' =>
-                Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-              Prod.snd ?inv).snd).fst
+                Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+              Prod.snd ?inv✝).snd).fst
       PUnit.unit
 [Elab.Tactic.Do.spec] discharge? ((fun a =>
             wp⟦pure (ForInStep.yield r✝)⟧
               (fun r =>
                 match r with
-                | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+                | ForInStep.yield b' =>
+                  Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
                 | ForInStep.done b' =>
-                  Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-                Prod.snd ?inv),
+                  Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+                Prod.snd ?inv✝),
             (fun r =>
                 match r with
-                | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+                | ForInStep.yield b' =>
+                  Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
                 | ForInStep.done b' =>
-                  Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-                Prod.snd ?inv).snd).fst
+                  Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+                Prod.snd ?inv✝).snd).fst
         PUnit.unit).down
 [Elab.Tactic.Do.spec] pure Prop: ((fun a =>
             wp⟦pure (ForInStep.yield r✝)⟧
               (fun r =>
                 match r with
-                | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+                | ForInStep.yield b' =>
+                  Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
                 | ForInStep.done b' =>
-                  Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-                Prod.snd ?inv),
+                  Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+                Prod.snd ?inv✝),
             (fun r =>
                 match r with
-                | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+                | ForInStep.yield b' =>
+                  Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
                 | ForInStep.done b' =>
-                  Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-                Prod.snd ?inv).snd).fst
+                  Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+                Prod.snd ?inv✝).snd).fst
         PUnit.unit).down
 [Elab.Tactic.Do.spec] Candidates for pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.pure]
 [Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
 [Elab.Tactic.Do.spec] Specs for pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.pure]
 [Elab.Tactic.Do.spec] dischargeMGoal: (fun r =>
           match r with
-          | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-          | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-          Prod.snd ?inv).fst
+          | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+          | ForInStep.done b' => Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+          Prod.snd ?inv✝).fst
       (ForInStep.yield r✝)
 [Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun r =>
           match r with
-          | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-          | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-          Prod.snd ?inv).fst
+          | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+          | ForInStep.done b' => Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+          Prod.snd ?inv✝).fst
       (ForInStep.yield r✝)
 [Elab.Tactic.Do.spec] discharge? ((fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv).fst
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝).fst
         (ForInStep.yield r✝)).down
 [Elab.Tactic.Do.spec] pure Prop: ((fun r =>
             match r with
-            | ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
-            | ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
-            Prod.snd ?inv).fst
+            | ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
+            | ForInStep.done b' =>
+              Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
+            Prod.snd ?inv✝).fst
         (ForInStep.yield r✝)).down
 [Elab.Tactic.Do.spec] Candidates for pure r✝.toArray: [SpecProof.global Std.Do.Spec.pure]
 [Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄

tests/elab/ppMVarsDocstrings.lean

@@ -0,0 +1,170 @@
+import Lean
+/-!
+# Synthetic tests of the dynamic docstrings for metavariables
+-/
+
+set_option linter.unusedVariables false
+
+open Lean Elab Tactic
+
+elab "#delab_docstrings " t:term : command => Command.runTermElabM fun _ => do
+  let e ← Term.elabTerm t none
+  Term.synthesizeSyntheticMVars (postpone := .partial)
+  logInfo m!"Expression: {e}"
+  let { infos, .. } ← Meta.ppExprWithInfos e
+  let infos := Array.qsort infos.toArray (lt := fun (p, _) (p', _) => p < p')
+  for (p, info) in infos do
+    if let .ofDelabTermInfo ti := info then
+      if let some doc ← ti.docString? (← Meta.getPPContext) then
+        let header ← Meta.withLCtx ti.lctx {} do
+          addMessageContext m!"{ti.expr}"
+        logInfo m!"{p}. {header}\n{doc}"
+
+/-!
+Natural metavariable.
+-/
+/--
+info: Expression: ?m.2
+---
+info: 1. ?m.2
+A metavariable representing an expression that should be solved for by unification during the elaboration process. They are created during elaboration as placeholders for implicit arguments and by `_` placeholder syntax.
+-/
+#guard_msgs in #delab_docstrings _
+
+/-!
+Synthetic opaque metavariable.
+-/
+/--
+info: Expression: ?m.2
+---
+info: 1. ?m.2
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+-/
+#guard_msgs in #delab_docstrings ?_
+
+/-!
+A synthetic metavariable and a natural metavariable.
+-/
+/--
+info: Expression: @default ?m.1 ?m.2
+---
+info: 5. ?m.2
+A metavariable representing a typeclass instance whose synthesis is still pending. They can be solved for by unification during the elaboration process, but the inferred expression and the synthesized instance must be definitionally equal.
+---
+info: 17. ?m.1
+A metavariable representing an expression that should be solved for by unification during the elaboration process. They are created during elaboration as placeholders for implicit arguments and by `_` placeholder syntax.
+-/
+#guard_msgs in set_option pp.explicit true in #delab_docstrings default
+
+/-!
+A delayed assignment pointing at a synthetic opaque metavariable.
+-/
+/--
+info: Expression: fun n => ?foo
+---
+info: 5. ?foo
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+This metavariable appears here via a *delayed assignment*. Substitution is delayed until the metavariable's value contains no metavariables, since all occurrences of the variables from its local context will need to be replaced with expressions that are valid in the current context.
+
+Additional variable in this metavariable's local context: `n`
+-/
+#guard_msgs in #delab_docstrings fun (n : Nat) => ?foo
+
+/-!
+An assigned synthetic opaque metavariable that can't be instantiated due to a metavariable.
+-/
+/--
+info: Expression: let f := fun b => ?_;
+f true
+---
+info: 21. ?_
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+This metavariable has been assigned, but it appears here via a *delayed assignment*. Substitution is delayed until the metavariable's value contains no metavariables, since all occurrences of the variables from its local context will need to be replaced with expressions that are valid in the current context. Substitution is awaiting assignment of the following metavariable: `?foo`
+
+Additional variable in this metavariable's local context: `b`
+-/
+#guard_msgs in
+set_option pp.mvars.anonymous false in
+#delab_docstrings
+  let f := fun (b : _) => if b then ?foo else true
+  f true
+
+elab "#delab_docstrings " t:term : tactic => withMainContext do
+  let e ← Tactic.elabTerm t none
+  logInfo m!"{e}"
+  let { infos, .. } ← Meta.ppExprWithInfos e
+  let infos := Array.qsort infos.toArray (lt := fun (p, _) (p', _) => p < p')
+  for (p, info) in infos do
+    if let .ofDelabTermInfo ti := info then
+      if let some doc ← ti.docString? (← Meta.getPPContext) then
+        let header ← Meta.withLCtx ti.lctx {} do
+          addMessageContext m!"{ti.expr}"
+        logInfo m!"{p}. {header}\n{doc}"
+
+/-!
+Metavariable shadowing. The `case'` tactic creates a new metavariablewith the same name.
+This causes the original one to print as `?foo✝` and to report that the name is unreachable.
+-/
+/--
+info: fun x => ?foo
+---
+info: 5. ?foo
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+This metavariable appears here via a *delayed assignment*. Substitution is delayed until the metavariable's value contains no metavariables, since all occurrences of the variables from its local context will need to be replaced with expressions that are valid in the current context.
+
+Additional variable in this metavariable's local context: `x`
+---
+info: fun x => ?foo✝
+---
+info: 5. ?foo✝
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+This metavariable has a name but it is unreachable.
+
+This metavariable has been assigned, but it appears here via a *delayed assignment*. Substitution is delayed until the metavariable's value contains no metavariables, since all occurrences of the variables from its local context will need to be replaced with expressions that are valid in the current context. Substitution is awaiting assignment of the following metavariable: `?foo`
+
+Additional variable in this metavariable's local context: `x`
+---
+info: fun x => 0 + 1
+-/
+#guard_msgs in
+example : True := by
+  let f : Nat → Nat := fun x => ?foo
+  #delab_docstrings value_of% f
+  case' foo => refine ?_ + 1
+  all_goals try #delab_docstrings value_of% f
+  exact 0
+  #delab_docstrings value_of% f
+  trivial
+
+/-!
+Checking that metavariables report which variables are absent from their local contexts.
+-/
+/--
+info: (?foo1, ?foo2, ?foo3)
+---
+info: 17. ?foo1
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+Variables absent from this metavariable's local context: `x`, `y`, `z`
+---
+info: 21. ?foo3
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+Variable absent from this metavariable's local context: `z`
+---
+info: 81. ?foo2
+A metavariable representing a tactic goal or an expression whose elaboration is still pending. They usually act like constants until they are completely solved for. They can be created using `?_` and `?n` synthetic placeholder syntax.
+
+Variables absent from this metavariable's local context: `y`, `z`
+-/
+#guard_msgs in
+example : True := by
+  let x : Nat := ?foo1
+  let y : Nat := ?foo2
+  let z : Nat := ?foo3
+  #delab_docstrings (value_of% x, value_of% y, value_of% z)
+  all_goals exact default

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/lake/tests/emptyBuild/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out

tests/lake/tests/emptyBuild/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+lean_lib Lib where
+  globs := #[]

tests/lake/tests/emptyBuild/lakefile.toml

@@ -0,0 +1,5 @@
+name = "test"
+
+[[lean_lib]]
+name = "Lib"
+globs = []

tests/lake/tests/emptyBuild/test.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+# This test covers the behavior of `lake build`
+# with no default targets configured.
+
+test_empty_build() {
+cfg_file=$1
+test_run -f $cfg_file update
+test_out_diff <(cat << 'EOF'
+warning: no targets specified and no default targets configured
+  Note: This will be an error in a future version of Lake.
+  Hint: This warning (or error) can be suppressed with '--allow-empty'.
+Nothing to build.
+EOF
+) -f $cfg_file build
+test_err_diff <(cat << 'EOF'
+warning: no targets specified and no default targets configured
+  Note: This will be an error in a future version of Lake.
+  Hint: This warning (or error) can be suppressed with '--allow-empty'.
+EOF
+) -f $cfg_file build --wfail
+test_out_diff <(cat << 'EOF'
+Nothing to build.
+EOF
+) -f $cfg_file build --allow-empty --wfail
+# Test the warning is not printed on a regular build.
+# The configurations use `globs = []` to minimize build variance,
+# and to verify that empty globs do not count as no jobs.
+test_out_diff <(cat << 'EOF'
+Build completed successfully (1 job).
+EOF
+) -f $cfg_file build Lib
+}
+
+# Test Lean configuration with no default targets
+./clean.sh
+echo "# TEST: lakefile.lean"
+test_empty_build lakefile.lean
+
+# Test TOML configuration with no default targets
+./clean.sh
+echo "# TEST: lakefile.toml"
+test_empty_build lakefile.toml
+
+# Cleanup
+rm -f produced.*