fix: do not bump transparency to instances in eqn LHS whnf (#13512)

This PR changes `whnfAux` in the equation-theorem generation machinery
to use
reducible transparency (`whnfR`) instead of instances transparency
(`whnfI`).
Previously, the loop in `Eqns.go` would unfold instances on the LHS,
which
interacts badly with users that mark `dite`/`ite` as
`implicit_reducible`:
equation generation would reduce past the `dite` and get stuck instead
of
committing to a branch. The original motivation for `whnfI` (reducing
`Nat.rec ... (OfNat.ofNat 0)` residuals from `match` on numeric
literals) is
already covered by the surrounding
`simpMatch?`/`simpIf?`/`simpTargetStar`
steps in `Eqns.go`, so the full test suite continues to pass.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

CMakeLists.txt

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

src/Init.lean

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

src/Init/Linter.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Init.Notation
+
+public section
+
+/-- `@[builtin_nolint linterName*]` omits the tagged declaration from being checked by
+the named builtin linters in `lake builtin-lint`. -/
+syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr

src/Lean/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/BuiltinDo/Match.lean

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

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -19,13 +19,20 @@ open Lean.Parser.Term
 /--
 Builtin do-element elaborator for `repeat` (syntax kind `Lean.Parser.Term.doRepeat`).
 
-Expands to `for _ in Loop.mk do ...`. A follow-up change will extend this
-elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a
-configuration option.
+Expands to `for _ in Loop.mk do ...`. When the body cannot `break`, the loop's own expression
+type is fixed to `PUnit`, yet the surrounding do block may require a different result type;
+we append an `unreachable!` so the continuation has a polymorphic value of any type. The
+`unreachable!` is never actually executed (the loop never terminates normally), and any
+dead-code warning that fires on the surrounding continuation is actionable — the user can
+remove the following code without breaking the do block's type.
 -/
 @[builtin_doElem_elab Lean.Parser.Term.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
   let `(doElem| repeat%$tk $seq) := stx | throwUnsupportedSyntax
-  let expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let mut expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let info ← inferControlInfoSeq seq
+  if !info.breaks then
+    if !(← Meta.isDefEqGuarded dec.resultType (← mkPUnit)) then
+      expanded ← `(doElem| do $expanded:doElem; unreachable!)
   Term.withMacroExpansion stx expanded <|
     withRef expanded <| elabDoElem ⟨expanded⟩ dec
 

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,6 +45,15 @@ 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. -/
@@ -90,9 +99,37 @@ 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
@@ -201,16 +238,7 @@ def mkPUnitUnit : DoElabM Expr := do
 
 /-- The expression ``pure (α:=α) e``. -/
 def mkPureApp (α e : Expr) : DoElabM Expr := 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
+  (← read).ops.toDoOps.mkPureApp α e
 
 /-- Create a `DoElemCont` returning the result using `pure`. -/
 def DoElemCont.mkPure (resultType : Expr) : TermElabM DoElemCont := do
@@ -229,13 +257,31 @@ def ReturnCont.mkPure (resultType : Expr) : TermElabM ReturnCont := do
 
 /-- The expression ``Bind.bind (α:=α) (β:=β) e k``. -/
 def mkBindApp (α β e k : Expr) : DoElabM Expr := 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
+  (← 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
 
 /-- Register the given name as that of a `mut` variable. -/
 def declareMutVar (x : Ident) (k : DoElabM α) : DoElabM α := do
@@ -434,18 +480,19 @@ 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 body'.isAppOfArity ``Pure.pure 4 && body'.getArg! 3 == xFVar then
-      let body'' ← mkPureApp eResultTy xFVar
-      if ← withNewMCtxDepth do isDefEq body' body'' then
-        return e
+    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
 
     -- 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 e'.isAppOfArity ``Pure.pure 4 then
-      let eRes := e'.getArg! 3
+    if let some eRes := ops.isPureApp? e' then
       let e' ← mkPureApp eResultTy eRes
       let (isPure, isDuplicable) ← withNewMCtxDepth do
         let isPure ← isDefEq e e'
@@ -587,7 +634,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x newX
-    withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
+    withDeadCode (if callerInfo.noFallthrough then .deadSemantically else .alive) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
@@ -683,11 +730,12 @@ 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) : TermElabM Context := do
+def mkContext (expectedType? : Option Expr) (ops : DoOps := .default) : TermElabM Context := do
   let (mi, resultType) ← extractMonadInfo expectedType?
   let returnCont ← ReturnCont.mkPure resultType
   let contInfo := ContInfo.toContInfoRef { returnCont }
-  return { monadInfo := mi, doBlockResultType := resultType, contInfo }
+  return { monadInfo := mi, doBlockResultType := resultType, contInfo,
+           ops := ops.toDoOpsRef }
 
 section NestedActions
 
@@ -903,11 +951,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."
 
--- @[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}"
+/-- Elaborate `doSeq` using `ops` for pure/bind construction. -/
+def elabDoWith (ops : DoOps) (doSeq : TSyntax ``doSeq)
+    (expectedType? : Option Expr) : TermElabM Expr := do
   Term.tryPostponeIfNoneOrMVar expectedType?
-  let ctx ← mkContext expectedType?
+  let ctx ← mkContext expectedType? (ops := ops)
   let cont ← DoElemCont.mkPure ctx.doBlockResultType
   let res ← elabDoSeq doSeq cont |>.run ctx
   -- Synthesizing default instances here is harmful for expressions such as
@@ -920,3 +968,8 @@ def elabDo : Term.TermElab := fun e expectedType? => do
   -- 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/Do/Control.lean

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

src/Lean/Elab/Do/InferControlInfo.lean

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

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/Elab/PreDefinition/EqnsUtils.lean

@@ -49,7 +49,7 @@ public def tryContradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.contradictionCore { genDiseq := true }
 
 partial def whnfAux (e : Expr) : MetaM Expr := do
-  let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
+  let e ← whnfR e
   let f := e.getAppFn
   match f with
   | .proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs

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/Lake/Load/Resolve.lean

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

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

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

tests/CMakeLists.txt

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

tests/bench/mvcgen/sym/run_test.sh

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

tests/elab/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/doControlInfoAggregate.lean

@@ -28,6 +28,9 @@ example (cond : Bool) : IO Nat := do
     return 42
   return 1
 
+/--
+warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
+-/
 #guard_msgs in
 example (i : Nat) : IO Nat := do
   for _ in [1, 2] do
@@ -66,11 +69,12 @@ example : IO Nat := do
     return 42
   return 1
 
--- Break-less `repeat` under both branches of an `if`. If `repeat` reported
--- `numRegularExits := 0`, the if's combined info would have `numRegularExits = 0` too, and the
--- dead-code warning would fire on `return 2`. The user cannot remove `return 2` though: the loop
--- expression is `Id PUnit`, so without a trailing element the do block's result type can't be
--- `Id Nat`. We therefore pin `repeat`'s `numRegularExits` at `1` (same as `for ... in`).
+-- Neither branch of the `if` can terminate normally, so the dead-code warning fires on
+-- `return 2`. The user can act on the warning: removing `return 2` still leaves the do block
+-- well-typed because `elabDoRepeat` injects an `unreachable!` into each branch's expansion.
+/--
+warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
+-/
 #guard_msgs in
 example (x : Nat) : Id Nat := do
   if x = 3 then
@@ -80,3 +84,22 @@ example (x : Nat) : Id Nat := do
     repeat
       pure ()
   return 2
+
+-- A break-less `repeat` whose body early-returns: `elabDoRepeat` injects an `unreachable!`, so
+-- the do block's `Id Nat` result type is recovered from the body's `return`.
+#guard_msgs in
+example (n : Nat) : Id Nat := do
+  let mut i := 0
+  repeat
+    if i = n then return i
+    i := i + 1
+
+-- Break-less, return-less `repeat` inside an action whose result type is polymorphic. The loop
+-- body never terminates, so `elabDoRepeat` leaves the expansion as a plain `for _ in Loop.mk`
+-- and the inner do block types as `m PUnit`, letting `BaseIO.asTask`'s polymorphic `α` resolve
+-- to `PUnit`.
+#guard_msgs in
+example : BaseIO Unit := do
+  let _ ← BaseIO.asTask do
+    repeat
+      pure ()

tests/elab/doNotationPluggableOps.lean

@@ -0,0 +1,217 @@
+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.*

tests/pkg/homo/Homo.lean

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

tests/pkg/homo/Homo/Init.lean

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

tests/pkg/homo/lakefile.lean

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

tests/pkg/homo/lean-toolchain

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

tests/pkg/homo/run_test.sh

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