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)

@[instance_reducible]

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

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.