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)) env.header.moduleNames

@[implicit_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.