max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: upstream environment linters to core lean (#13356)

Browse source 
This PR upstreams environment linters of batteries to core lean.
This commit is contained in:
Wojciech Różowski 2026-04-13 15:13:15 +02:00 • committed by GitHub
parent cd697eac81
commit 1c9e26420f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 581 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Linter.lean
View file

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

10
src/Lean/Linter/EnvLinter.lean Normal file
View file

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

163
src/Lean/Linter/EnvLinter/Basic.lean Normal file
View file

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

180
src/Lean/Linter/EnvLinter/Frontend.lean Normal file
View file

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

2
stage0/src/stdlib_flags.h
View file

@ -1,5 +1,5 @@
#include "util/options.h"
// Please update stage0
namespace lean {
options get_default_options() {
options opts;

226
tests/elab/env_linter.lean Normal file
View file

@ -0,0 +1,226 @@
import Lean
open Lean Linter EnvLinter Meta
/-! ## Dummy env linter for testing -/
/-- A dummy linter that flags any declaration whose last name component starts with "bad". -/
@[builtin_env_linter]
public meta def dummyBadName : EnvLinter where
test declName := do
if let .str _ s := declName then
if s.startsWith "bad" then
return some m!"declaration name starts with 'bad'"
return none
noErrorsFound := "no bad names found"
errorsFound := "found bad names"
/-! ## Test: extension registration -/
def testExtContains (name : Name) : CoreM Bool := do
let ext := envLinterExt.getState (← getEnv)
return ext.contains name
/-- info: true -/
#guard_msgs in
#eval testExtContains `dummyBadName
/-- info: false -/
#guard_msgs in
#eval testExtContains `nonexistentLinter
/-! ## Test: getEnvLinter resolves the linter -/
def testResolveLinter : CoreM String := do
let some (declName, _) := (envLinterExt.getState (← getEnv)).find? `dummyBadName
| throwError "not found"
let linter ← getEnvLinter `dummyBadName declName
return toString linter.name
/-- info: "dummyBadName" -/
#guard_msgs in
#eval testResolveLinter
/-! ## Test: dummy linter detects bad names -/
def badDef : Nat := 42
def goodDef : Nat := 42
def testLinterDetects (declName : Name) : MetaM Bool := do
let some (linterDeclName, _) := (envLinterExt.getState (← getEnv)).find? `dummyBadName
| throwError "not found"
let linter ← getEnvLinter `dummyBadName linterDeclName
return (← linter.test declName).isSome
/-- info: true -/
#guard_msgs in
#eval testLinterDetects `badDef
/-- info: false -/
#guard_msgs in
#eval testLinterDetects `goodDef
/-! ## Test: builtin_nolint -/
@[builtin_nolint dummyBadName]
def badButNolinted : Nat := 99
def testShouldBeLinted (linter decl : Name) : CoreM Bool := do
shouldBeLinted linter decl
/-- info: false -/
#guard_msgs in
#eval testShouldBeLinted `dummyBadName `badButNolinted
/-- info: true -/
#guard_msgs in
#eval testShouldBeLinted `dummyBadName `badDef
/-! ## Test: builtin_env_linter clippy -/
@[builtin_env_linter clippy]
public meta def dummyClippyLinter : EnvLinter where
test _ := return none
noErrorsFound := "ok"
errorsFound := "err"
-- The extension stores (declName, isDefault). Clippy-only means isDefault = false.
def testIsDefault (name : Name) : CoreM (Option Bool) := do
let ext := envLinterExt.getState (← getEnv)
match ext.find? name with
| some (_, isDefault) => return some isDefault
| none => return none
/-- info: some false -/
#guard_msgs in
#eval testIsDefault `dummyClippyLinter
/-- info: some true -/
#guard_msgs in
#eval testIsDefault `dummyBadName
/-! ## Test: duplicate linter name is rejected -/
/--
error: invalid attribute `builtin_env_linter`, linter `dummyBadName` has already been declared
-/
#guard_msgs in
@[builtin_env_linter] public meta def Other.dummyBadName : EnvLinter :=
{ test := fun _ => return none, noErrorsFound := "", errorsFound := "" }
/-! ## Test: isAutoDecl -/
/-- info: true -/
#guard_msgs in
#eval isAutoDecl `Nat.casesOn
/-- info: true -/
#guard_msgs in
#eval isAutoDecl `Nat.recOn
/-- info: false -/
#guard_msgs in
#eval isAutoDecl `Nat.add
/-! ## Test: getChecks -/
-- Default mode: only isDefault=true linters
def testGetChecksDefault : CoreM (Array Name) := do
let checks ← getChecks (clippy := false) (runOnly := none)
return checks.map (·.name)
-- dummyBadName is default, dummyClippyLinter is not
/-- info: #[`dummyBadName] -/
#guard_msgs in
#eval testGetChecksDefault
-- Clippy mode: all linters
def testGetChecksClippy : CoreM (Array Name) := do
let checks ← getChecks (clippy := true) (runOnly := none)
return checks.map (·.name)
/-- info: #[`dummyBadName, `dummyClippyLinter] -/
#guard_msgs in
#eval testGetChecksClippy
-- runOnly: only specified linters
def testGetChecksRunOnly : CoreM (Array Name) := do
let checks ← getChecks (clippy := false) (runOnly := some [`dummyClippyLinter])
return checks.map (·.name)
/-- info: #[`dummyClippyLinter] -/
#guard_msgs in
#eval testGetChecksRunOnly
/-! ## Test: getDeclsInCurrModule -/
def testDeclsInCurrModule : CoreM Bool := do
let decls ← getDeclsInCurrModule
-- Our test declarations should be in the current module
return decls.contains `badDef && decls.contains `goodDef && decls.contains `badButNolinted
/-- info: true -/
#guard_msgs in
#eval testDeclsInCurrModule
/-! ## Test: lintCore -/
-- lintCore should find badDef but not goodDef or badButNolinted
def testLintCore : CoreM (Array (Name × Nat)) := do
let linters ← getChecks (clippy := false) (runOnly := none)
let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
return results.map fun (linter, msgs) => (linter.name, msgs.size)
/-- info: #[(`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 results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
let mut flagged := #[]
for (_, msgs) in results do
for (name, _) in msgs.toArray do
flagged := flagged.push name
return flagged
/-- info: #[`badDef] -/
#guard_msgs in
#eval testLintCoreDetail
/-! ## Test: formatLinterResults -/
def testFormatResults : CoreM Format := do
let linters ← getChecks (clippy := false) (runOnly := none)
let results ← lintCore #[`badDef, `goodDef] linters
let msg ← formatLinterResults results #[`badDef, `goodDef]
(groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
(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
/- The `dummyBadName` linter reports:
found bad names -/
#check badDef /- declaration name starts with 'bad' -/
-/
#guard_msgs in
#eval testFormatResults
-- No errors case
def testFormatResultsClean : CoreM Format := do
let linters ← getChecks (clippy := false) (runOnly := none)
let results ← lintCore #[`goodDef] linters
let msg ← formatLinterResults results #[`goodDef]
(groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
(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
-/
#guard_msgs in
#eval testFormatResultsClean