structure Lean.Linter.LintEntry : Type

• linter : Name
• message : SerialMessage
• position? : Option Position
• file : String

opaque Lean.Linter.lintLogExt : PersistentEnvExtension LintEntry LintEntry (Array LintEntry)

def Lean.Linter.getAllLints (env : Environment) : Array (Name × Array LintEntry)

Equations

• Lean.Linter.getAllLints env = Array.mapIdx (fun (i : Nat) (mod : Lean.Name) => (mod, Lean.Linter.lintLogExt.getModuleEntries env i Lean.OLeanLevel.server)) env.header.moduleNames

structure Lean.Linter.CodeQualityLogEntry : Type

A code quality entry recorded into codeQualityLogExt, together with the option name of the linter that produced it. Entries logged via logCodeQualityEntryIf carry their linter's option name, which consumers use to filter by linter selection (e.g. lake lint --lint-only); entries logged via logCodeQualityEntry carry none and are exempt from such filtering.

• linter? : Option Name
• entry : CodeQuality.Entry

opaque Lean.Linter.codeQualityLogExt : PersistentEnvExtension CodeQualityLogEntry CodeQualityLogEntry (Array CodeQualityLogEntry)

def Lean.Linter.getAllCodeQualityEntries (env : Environment) : Array (Name × Array CodeQualityLogEntry)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Linter.instMonadFileMapReaderTFileMapBaseIO : MonadFileMap (ReaderT FileMap BaseIO)

Equations

• Lean.Linter.instMonadFileMapReaderTFileMapBaseIO = { getFileMap := read }

def Lean.Linter.recordLints (fileMap : FileMap) (env : Environment) (commandLints : Array (Option Syntax × MessageLog)) : BaseIO Environment

Records linter warnings and looks up positions of their associated commands from a build into lintLogExt so that consumers (e.g. lake lint) can recover them from the .olean.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Linter.logCodeQualityEntry {m : Type → Type} [Monad m] [MonadEnv m] (e : CodeQuality.Entry) : m Unit

Records the code quality entry e into codeQualityLogExt so that it is persisted into the .olean and can be recovered by consumers via getAllCodeQualityEntries.

This can be safely used in Linters. While regular Lean.Linters, module linters, and stateful linters all have their environment changes discarded after running, entries they log are captured per command (see Command.State.codeQualityEntryTasks) and merged into the final environment in runFrontend.

The entry is recorded without a linter attribution, so it is recorded unconditionally and no linter selection flag (e.g. lake lint --lint-only) can suppress it. Inside a linter guarded by an option, use logCodeQualityEntryIf instead; this variant is meant for unconditional metrics not tied to any linter option.

Equations

• Lean.Linter.logCodeQualityEntry e = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Linter.codeQualityLogExt.addEntry x { linter? := none, entry := e }

def Lean.Linter.logCodeQualityEntryIf {m : Type → Type} [Monad m] [MonadOptions m] [MonadEnv m] (linterOption : Lean.Option Bool) (e : CodeQuality.Entry) : m Unit

Similar to logLintIf, but for logCodeQualityEntry - i.e. it logs an entry only if the provided linter option is enabled, taking linter.all and linter sets into account. The entry is recorded with linterOption.name as its attribution, so consumers can filter it by linter selection (e.g. lake lint --lint-only).

Equations

• One or more equations did not get rendered due to their size.