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

structure Lean.Linter.CodeQuality.NamedPackageCheck : Type

• declName : Name
• run : PackageCheck

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

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

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

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