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 once per package; each check sees the whole environment and is responsible for restricting its metrics to the package named by the PackageCheckContext it receives. Registered 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.

structure Lean.Linter.CodeQuality.PackageCheckContext : Type

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

• pkgRoot : Name
• srcSearchPath : System.SearchPath

@[reducible, inline]

abbrev Lean.Linter.CodeQuality.PackageCheck : Type

Equations

• Lean.Linter.CodeQuality.PackageCheck = (Lean.Linter.CodeQuality.PackageCheckContext → Lean.MetaM (Array Lean.Linter.CodeQuality.Entry))

structure Lean.Linter.CodeQuality.NamedPackageCheck : Type

• declName : Name
• run : PackageCheck

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

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 (Array Entry)

Equations

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