chore: update stage0

This PR upstreams environment linters of batteries to core lean.

src/Lean/Linter.lean

@@ -19,3 +19,4 @@ public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
 public import Lean.Linter.GlobalAttributeIn
+public import Lean.Linter.EnvLinter

src/Lean/Linter/EnvLinter.lean

@@ -0,0 +1,10 @@
+/-
+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.Basic
+public import Lean.Linter.EnvLinter.Frontend

src/Lean/Linter/EnvLinter/Basic.lean

@@ -0,0 +1,163 @@
+/-
+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.Structure
+public import Lean.Elab.InfoTree.Main
+import Lean.ExtraModUses
+
+public section
+
+open Lean Meta
+
+namespace Lean.Linter.EnvLinter
+
+/-!
+# Basic environment linter types and attributes
+
+This file defines the basic types and attributes used by the environment
+linting framework. An environment linter consists of a function
+`(declaration : Name) → MetaM (Option MessageData)`, this function together with some
+metadata is stored in the `EnvLinter` structure. We define two attributes:
+
+ * `@[builtin_env_linter]` applies to a declaration of type `EnvLinter`
+   and adds it to the default linter set.
+
+ * `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
+   the linter with name `linterName`.
+-/
+
+/--
+Returns true if `decl` is an automatically generated declaration.
+
+Also returns true if `decl` is an internal name or created during macro
+expansion.
+-/
+def isAutoDecl (decl : Name) : CoreM Bool := do
+  if decl.hasMacroScopes then return true
+  if decl.isInternal then return true
+  let env ← getEnv
+  if isReservedName env decl then return true
+  if let Name.str n s := decl then
+    if (← isAutoDecl n) then return true
+    if s.startsWith "proof_"
+        || s.startsWith "match_"
+        || s.startsWith "unsafe_"
+        || s.startsWith "grind_"
+    then return true
+    if env.isConstructor n && s ∈ ["injEq", "inj", "sizeOf_spec", "elim", "noConfusion"] then
+      return true
+    if let ConstantInfo.inductInfo _ := env.find? n then
+      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
+      if s ∈ [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
+          "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx", "ctorIdx",
+          "ctorElim", "ctorElimType"] then
+        return true
+      if let some _ := isSubobjectField? env n (.mkSimple s) then
+        return true
+    -- Coinductive/inductive lattice-theoretic predicates:
+    if let ConstantInfo.inductInfo _ := env.find? (Name.str n "_functor") then
+      if s == "functor_unfold" || s == casesOnSuffix || s == "mutual" then return true
+      if env.isConstructor (Name.str (Name.str n "_functor") s) then return true
+  pure false
+
+/-- An environment linting test for the `lake builtin-lint` command. -/
+structure EnvLinter where
+  /-- `test` defines a test to perform on every declaration. It should never fail. Returning `none`
+  signifies a passing test. Returning `some msg` reports a failing test with error `msg`. -/
+  test : Name → MetaM (Option MessageData)
+  /-- `noErrorsFound` is the message printed when all tests are negative -/
+  noErrorsFound : MessageData
+  /-- `errorsFound` is printed when at least one test is positive -/
+  errorsFound : MessageData
+  /-- If `isDefault` is false, this linter is only run when `--clippy` is passed. -/
+  isDefault := true
+
+/-- A `NamedEnvLinter` is an environment linter associated to a particular declaration. -/
+structure NamedEnvLinter extends EnvLinter where
+  /-- The name of the named linter. This is just the declaration name without the namespace. -/
+  name : Name
+  /-- The linter declaration name -/
+  declName : Name
+
+/-- Gets an environment linter by declaration name. -/
+def getEnvLinter (name declName : Name) : CoreM NamedEnvLinter := unsafe
+  return { ← evalConstCheck EnvLinter ``EnvLinter declName with name, declName }
+
+/-- Defines the `envLinterExt` extension for adding an environment linter to the default set. -/
+builtin_initialize envLinterExt :
+    SimplePersistentEnvExtension (Name × Bool) (NameMap (Name × Bool)) ←
+  let addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
+  registerSimplePersistentEnvExtension {
+    addImportedFn := fun nss =>
+      nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
+    addEntryFn
+  }
+
+/--
+Defines the `@[builtin_env_linter]` attribute for adding a linter to the default set.
+The form `@[builtin_env_linter clippy]` will not add the linter to the default set,
+but it can be selected by `lake builtin-lint --clippy`.
+
+Linters are named using their declaration names, without the namespace. These must be distinct.
+-/
+syntax (name := builtin_env_linter) "builtin_env_linter" &" clippy"? : attr
+
+builtin_initialize registerBuiltinAttribute {
+  name := `builtin_env_linter
+  descr := "Use this declaration as a linting test in `lake builtin-lint`"
+  add   := fun decl stx kind => do
+    let dflt := stx[1].isNone
+    unless kind == .global do throwError "invalid attribute `builtin_env_linter`, must be global"
+    let shortName := decl.updatePrefix .anonymous
+    if let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName then
+      Elab.addConstInfo stx declName
+      throwError
+        "invalid attribute `builtin_env_linter`, linter `{shortName}` has already been declared"
+    let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta (← getEnv) decl
+    unless isPublic && isMeta do
+      throwError "invalid attribute `builtin_env_linter`, \
+        declaration `{.ofConstName decl}` must be marked as `public` and `meta`\
+        {if isPublic then " but is only marked `public`" else ""}\
+        {if isMeta then " but is only marked `meta`" else ""}"
+    let constInfo ← getConstInfo decl
+    unless ← (isDefEq constInfo.type (mkConst ``EnvLinter)).run' do
+      throwError "`{.ofConstName decl}` must have type `{.ofConstName ``EnvLinter}`, got \
+        `{constInfo.type}`"
+    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/Frontend.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Linter.EnvLinter.Basic
+import Lean.DeclarationRange
+import Lean.Util.Path
+import Lean.CoreM
+import Lean.Elab.Command
+
+public section
+
+open Lean Meta
+
+namespace Lean.Linter.EnvLinter
+
+/-- Verbosity for the linter output. -/
+inductive LintVerbosity
+  /-- `low`: only print failing checks, print nothing on success. -/
+  | low
+  /-- `medium`: only print failing checks, print confirmation on success. -/
+  | medium
+  /-- `high`: print output of every check. -/
+  | 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)) :
+    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
+    if shouldRun then
+      let linter ← getEnvLinter name declName
+      result := result.binInsert (·.name.lt ·.name) linter
+  pure result
+
+
+/--
+Runs all the specified linters on all the specified declarations in parallel,
+producing a list of results.
+-/
+def lintCore (decls : Array Name) (linters : Array NamedEnvLinter) :
+    CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData)) := do
+  let tasks : Array (NamedEnvLinter × Array (Name × Task (Except Exception <| Option MessageData))) ←
+    linters.mapM fun linter => do
+      let decls ← decls.filterM (shouldBeLinted linter.name)
+      (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
+        let act : MetaM (Option MessageData) := do
+          linter.test decl
+        EIO.asTask <| (← Core.wrapAsync (fun _ =>
+          act |>.run' Elab.Command.mkMetaContext
+        ) (cancelTk? := none)) ()
+
+  let result ← tasks.mapM fun (linter, decls) => do
+    let mut msgs : Std.HashMap Name MessageData := {}
+    for (declName, msgTask) in decls do
+      let msg? ← match msgTask.get with
+      | Except.ok msg? => pure msg?
+      | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
+      if let .some msg := msg? then
+        msgs := msgs.insert declName msg
+    pure (linter, msgs)
+  return result
+
+/-- Sorts a map with declaration keys as names by line number. -/
+def sortResults (results : Std.HashMap Name α) : CoreM <| Array (Name × α) := do
+  let mut key : Std.HashMap Name Nat := {}
+  for (n, _) in results.toArray do
+    if let some range ← findDeclarationRanges? n then
+      key := key.insert n <| range.range.pos.line
+  pure $ results.toArray.qsort fun (a, _) (b, _) => key.getD a 0 < key.getD b 0
+
+/-- Formats a linter warning as `#check` command with comment. -/
+def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false)
+  (filePath : System.FilePath := default) : CoreM MessageData := do
+  if useErrorFormat then
+    if let some range ← findDeclarationRanges? declName then
+      let msg ← addMessageContextPartial
+        m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: {
+          ← mkConstWithLevelParams declName} {warning}"
+      return msg
+  addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
+
+/-- Formats a map of linter warnings using `printWarning`, sorted by line number. -/
+def printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default)
+    (useErrorFormat : Bool := false) : CoreM MessageData := do
+  (MessageData.joinSep ·.toList Format.line) <$>
+    (← sortResults results).mapM fun (declName, warning) =>
+      printWarning declName warning (useErrorFormat := useErrorFormat) (filePath := filePath)
+
+/--
+Formats a map of linter warnings grouped by filename with `-- filename` comments.
+-/
+def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) :
+    CoreM MessageData := do
+  let sp ← if useErrorFormat then getSrcSearchPath else pure {}
+  let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ←
+    results.foldM (init := {}) fun grouped declName msg => do
+      let mod ← findModuleOf? declName
+      let mod := mod.getD (← getEnv).mainModule
+      grouped.insert mod <$>
+        match grouped[mod]? with
+        | some (fp, msgs) => pure (fp, msgs.insert declName msg)
+        | none => do
+          let fp ← if useErrorFormat then
+            pure <| (← sp.findWithExt "lean" mod).getD (modToFilePath "." mod "lean")
+          else pure default
+          pure (fp, .insert {} declName msg)
+  let grouped' := grouped.toArray.qsort fun (a, _) (b, _) => toString a < toString b
+  (MessageData.joinSep · (Format.line ++ Format.line)) <$>
+    grouped'.toList.mapM fun (mod, fp, msgs) => do
+      pure m!"-- {mod}\n{← printWarnings msgs (filePath := fp) (useErrorFormat := useErrorFormat)}"
+
+/--
+Formats the linter results as Lean code with comments and `#check` commands.
+-/
+def formatLinterResults
+    (results : Array (NamedEnvLinter × Std.HashMap Name MessageData))
+    (decls : Array Name)
+    (groupByFilename : Bool)
+    (whereDesc : String) (runClippyLinters : Bool)
+    (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) :
+    CoreM MessageData := do
+  let formattedResults ← results.filterMapM fun (linter, results) => do
+    if !results.isEmpty then
+      let warnings ←
+        if groupByFilename || useErrorFormat then
+          groupedByFilename results (useErrorFormat := useErrorFormat)
+        else
+          printWarnings results
+      pure $ some m!"/- The `{linter.name}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n"
+    else if verbose = LintVerbosity.high then
+      pure $ some m!"/- OK: {linter.noErrorsFound} -/"
+    else
+      pure none
+  let mut s := MessageData.joinSep formattedResults.toList Format.line
+  let numAutoDecls := (← decls.filterM isAutoDecl).size
+  let failed := results.map (·.2.size) |>.foldl (·+·) 0
+  unless verbose matches LintVerbosity.low do
+    s := m!"-- Found {failed} error{if failed == 1 then "" else "s"
+      } 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"
+  pure s
+
+/-- Get the list of declarations in the current module. -/
+def getDeclsInCurrModule : CoreM (Array Name) := do
+  pure $ (← getEnv).constants.map₂.foldl (init := #[]) fun r k _ => r.push k
+
+/-- Get the list of all declarations in the environment. -/
+def getAllDecls : CoreM (Array Name) := do
+  pure $ (← getEnv).constants.map₁.fold (init := ← getDeclsInCurrModule) fun r k _ => r.push k
+
+/-- Get the list of all declarations in the specified package. -/
+def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
+  let env ← getEnv
+  let mut decls ← getDeclsInCurrModule
+  let modules := env.header.moduleNames.map (pkg.isPrefixOf ·)
+  return env.constants.map₁.fold (init := decls) fun decls declName _ =>
+    if modules[env.const2ModIdx[declName]?.get!]! then
+      decls.push declName
+    else decls
+
+end Lean.Linter.EnvLinter