Code quality check registration and driver

A package code quality check is a declaration of type PackageCheck tagged with the @[package_code_quality_check] attribute. The driver runs every registered check, providing it with the data encapsulated in PackageCheckContext. All checks are tracked by the packageCheckExt environment extension and are run concurrently, one task per check, by runPackageChecks, which combines all results into a single array of entries and accumulates all errors.

structure Lean.Linter.CodeQuality.PackageCheckContext : Type

Global inputs provided by the driver to every code quality check.

• srcSearchPath : System.SearchPath
• topLevelModule : Name

structure Lean.Linter.CodeQuality.PackageCheck : Type

• ofFn :: (
• run : PackageCheckContext → MetaM (Array Entry)
• )

structure Lean.Linter.CodeQuality.CheckResult : Type

• entries : Array Entry
• errors : Array MessageData

structure Lean.Linter.CodeQuality.NamedPackageCheckextends Lean.Linter.CodeQuality.PackageCheck : Type

• run : PackageCheckContext → MetaM (Array Entry)
• declName : Name

def Lean.Linter.CodeQuality.getPackageCheck (declName : Name) : CoreM NamedPackageCheck

Equations

• Lean.Linter.CodeQuality.getPackageCheck declName = Lean.Linter.CodeQuality.getPackageCheck.unsafe_impl_2✝ declName

opaque Lean.Linter.CodeQuality.packageCheckExt : SimplePersistentEnvExtension Name (Array Name)

def Lean.Linter.CodeQuality.getPackageChecks : CoreM (Array NamedPackageCheck)

Equations

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

def Lean.Linter.CodeQuality.runPackageChecks (checks : Array NamedPackageCheck) (ctx : PackageCheckContext) : CoreM CheckResult

Equations

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