feat: lake: support package code quality checks in lake lint

src/Lean/Linter/CodeQuality/Basic.lean

@@ -8,10 +8,8 @@ module
 
 prelude
 
-public import Init.Data.Float
-public import Std.Data.TreeMap
-public import Init.Data.Ord
 public import Lean.Data.Json
+public import Lean.Message
 
 public section
 
@@ -33,4 +31,8 @@ structure Entry where
   value : Value
   deriving ToJson
 
+structure CheckResult where
+  entries : Array Entry
+  errors : Array MessageData
+
 end Lean.Linter.CodeQuality

src/Lean/Linter/CodeQuality/Frontend.lean

@@ -6,10 +6,8 @@ Authors: Wojciech Różowski
 module
 
 prelude
-public import Init.System.FilePath
 public import Lean.Linter.CodeQuality.Basic
 public import Lean.Elab.InfoTree.Main
-import Lean.CoreM
 import Lean.Elab.Command
 
 public section
@@ -22,28 +20,26 @@ namespace Lean.Linter.CodeQuality
 # 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.
+`@[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.
 -/
 
-
 /-- Global inputs provided by the driver to every code quality check. -/
 structure PackageCheckContext where
-  pkgRoot : Name
-  srcSearchPath : System.SearchPath := {}
+  srcSearchPath : System.SearchPath
+  topLevelModule : Name
 
-abbrev PackageCheck := PackageCheckContext → MetaM (Array Entry)
+structure PackageCheck where
+  run : PackageCheckContext → MetaM (Array Entry)
 
-structure NamedPackageCheck where
+structure NamedPackageCheck extends PackageCheck where
   declName : Name
-  run : PackageCheck
 
-def getPackageCheck (declName : Name) : CoreM PackageCheck := unsafe
-  evalConstCheck PackageCheck ``PackageCheck declName
+def getPackageCheck (declName : Name) : CoreM NamedPackageCheck := unsafe
+  return { ← evalConstCheck PackageCheck ``PackageCheck declName with declName}
 
 builtin_initialize packageCheckExt : SimplePersistentEnvExtension Name (Array Name) ←
   registerSimplePersistentEnvExtension {
@@ -72,21 +68,24 @@ builtin_initialize registerBuiltinAttribute {
 }
 
 def getPackageChecks : CoreM (Array NamedPackageCheck) := do
-  (packageCheckExt.getState (← getEnv)).mapM fun declName =>
-    return { declName, run := ← getPackageCheck declName }
+  let mut result := #[]
+  for declName in packageCheckExt.getState (← getEnv) do
+    let linter ← getPackageCheck declName
+    result := result.binInsert (·.declName.lt ·.declName) linter
+  pure result
 
 def runPackageChecks (checks : Array NamedPackageCheck) (ctx : PackageCheckContext) :
-    CoreM (Array Entry) := do
+    CoreM CheckResult := do
   let tasks ← checks.mapM fun check => do
-    (check.declName, ·) <$> (EIO.asTask <| (← Core.wrapAsync (fun _ =>
+    let act ← Core.wrapAsync (cancelTk? := none) fun (_ : Unit) =>
       check.run ctx |>.run' Elab.Command.mkMetaContext
-    ) (cancelTk? := none)) ())
+    return (check.declName, ← EIO.asTask (act ()))
   let mut entries := #[]
+  let mut errors := #[]
   for (declName, task) in tasks do
     match task.get with
     | .ok checkEntries => entries := entries ++ checkEntries
-    | .error err =>
-      IO.eprintln s!"code quality check `{declName}` failed: {← err.toMessageData.toString}"
-  return entries
+    | .error err => errors := errors.push (s!"{declName} has failed: " ++ err.toMessageData)
+  return ⟨entries, errors⟩
 
 end Lean.Linter.CodeQuality

src/lake/Lake/CLI/BuiltinLint.lean

@@ -8,10 +8,7 @@ module
 prelude
 public import Lean.Linter.EnvLinter
 public import Lean.Linter.PersistentLintLog
-import Lean.CoreM
-import Lean.DocString.Extension
 import Lean.Elab.DocString.Builtin.Postponed
-import Lake.Config.Workspace
 import Lean.Linter.CodeQuality
 
 open Lean Lean.Core Meta Linter
@@ -44,6 +41,9 @@ public structure Args where
   /-- Whether to record linter warnings as `set_option <linter> false in` exceptions
   by editing the source files in place. -/
   mode : Mode := .report
+  /-- An array of modules containing code quality checks that are
+  imported alongside each top-level module -/
+  checks : Array Name := #[]
   /-- Source search path used to resolve modules to their `.lean` files when recording
   exceptions for environment linters. Populated from the workspace's `LEAN_SRC_PATH`, since
   `getSrcSearchPath` alone does not cover package sources during a `lake lint` run. -/
@@ -99,6 +99,10 @@ private inductive DeferredCheckOutcome where
   -/
   | recorded (records : Array ExceptionRecord) (unlocated : Bool)
 
+private structure PackageCodeQualityCheckOutcome where
+  entries : Array CodeQuality.Entry
+  failed : Bool
+
 private def collectTextLints
     (env : Environment) (pkgRoot : Name) :
     Array (Name × Array Linter.LintEntry) :=
@@ -383,12 +387,27 @@ private def runEnvironmentLinters (args : Args) (linterOpts : Linter.LinterOptio
       return .codeQualityChecks codeQualityEntries
   return outcome
 
+private def runPackageCodeQualityChecks (sp : SearchPath) (env : Environment)
+    (mod : Name) : IO PackageCodeQualityCheckOutcome := do
+  let ⟨(outcome, anyFailed), _⟩ ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
+    let mut anyFailed : Bool := false
+    let checks ← CodeQuality.getPackageChecks
+    let ⟨outcome, errors⟩ ← CodeQuality.runPackageChecks checks
+      { srcSearchPath := sp, topLevelModule := mod }
+    if !errors.isEmpty then
+      anyFailed := true
+    for error in errors do
+      IO.eprintln (← error.format)
+    return (outcome, anyFailed)
+  return ⟨outcome, anyFailed⟩
+
 public def run (args : Args) : IO UInt32 := do
   let mods := args.mods
   if mods.isEmpty then
     IO.eprintln "lake lint: no modules specified for builtin linting"
     return 1
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
+  let checkImports : Array Import := args.checks.map fun c => { module := c }
 
   let sp := args.srcSearchPath ++ (← getSrcSearchPath)
 
@@ -412,7 +431,7 @@ public def run (args : Args) : IO UInt32 := do
     let isModule ← getIsModule modData
     let level := if isModule then OLeanLevel.server else OLeanLevel.private
     unsafe region.free
-    let env ← importModules #[{ module := mod }, envLinterModule] {}
+    let env ← importModules (#[{ module := mod }, envLinterModule] ++ checkImports) {}
       (trustLevel := 1024) (loadExts := true) (level := level)
 
     -- We create `LinterOptions` out of the passed overrides
@@ -442,7 +461,11 @@ public def run (args : Args) : IO UInt32 := do
     | .codeQualityChecks entries =>
       codeQualityEntries := codeQualityEntries ++ entries
 
-    unless args.mode == .codeQuality do
+    if args.mode == .codeQuality then
+      let ⟨entries, failed⟩ ← runPackageCodeQualityChecks sp env mod
+      codeQualityEntries := codeQualityEntries ++ entries
+      if failed then anyFailed := true
+    else
       let deferredResults ← runDeferredChecks args linterOpts sp env mod.getRoot docCheckedModules
       docCheckedModules := deferredResults.checkedModules
       match deferredResults.outcome with
@@ -461,6 +484,6 @@ public def run (args : Args) : IO UInt32 := do
   | .codeQuality =>
     for entry in codeQualityEntries do
       IO.println <| toJson entry
-    return 0
+    return if anyFailed then 1 else 0
 
 end Lake.BuiltinLint

src/lake/Lake/CLI/Help.lean

@@ -290,6 +290,9 @@ OPTIONS:
   --code-quality        records each linter warning as a code quality check result
                         and runs the registered code quality checks.
                         Setting this flag will skip lint driver.
+  --checks <mods>       comma-separated list of workspace modules providing
+                        package code quality checks; they are imported
+                        alongside each linted module (implies --code-quality)
 
 A lint driver can be configured by either setting the `lintDriver` package
 configuration option or by tagging a script or executable `@[lint_driver]`.

src/lake/Lake/CLI/Main.lean

@@ -363,6 +363,17 @@ def lakeLongOption : (opt : String) → CliM PUnit
     modifyLintOnlyFlag true
   let spec ← takeOptArg "--lint-only" "comma-separated linter spec"
   parseLintersSpec spec
+| "--checks" => do
+  let spec ← takeOptArg "--checks" "comma-separated module names"
+  let mut checks : Array Lean.Name := #[]
+  for raw in spec.split (· == ',') do
+    let s := raw.trimAscii
+    unless s.isEmpty do
+      checks := checks.push s.toName
+  modifyThe LakeOptions fun opts =>
+    { opts with runBuiltinLint := true, builtinOnly := true,
+                builtinLint.checks := opts.builtinLint.checks ++ checks,
+                builtinLint.mode := .codeQuality }
 
 -- Shared options
 | "--force" => modifyThe LakeOptions ({· with shake.force := true})
@@ -1036,8 +1047,15 @@ private def runBuiltinLint
   if mods.isEmpty then
     error "no modules specified and there are no applicable default targets"
   let args := opts.builtinLint
-  let args := {args with mods, srcSearchPath := ws.augmentedLeanSrcPath}
-  let specs ← parseTargetSpecs ws (mods.map (s!"+{·}") |>.toList)
+  let checks := (ws.root.config.checks ++ args.checks).foldl (init := #[])
+    fun acc c => if acc.contains c then acc else acc.push c
+  for c in checks do
+    unless (ws.findTargetModule? c).isSome do
+      error s!"unknown checks module `{c}`; it must be a module of a package in the workspace"
+  let args := { args with mods, checks, srcSearchPath := ws.augmentedLeanSrcPath }
+  -- Checks modules are imported alongside each lint target, so they must be built as well.
+  let buildMods := mods ++ checks.filter (!mods.contains ·)
+  let specs ← parseTargetSpecs ws (buildMods.map (s!"+{·}") |>.toList)
   let lintOpts := BuiltinLint.leanOptOverrides args
   let overrides : Lean.NameMap Lean.LeanOptions :=
     if lintOpts.values.isEmpty then

src/lake/Lake/Config/PackageConfig.lean

@@ -335,6 +335,11 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
     as a fallback).
   -/
   builtinLint?, builtinLint : Option Bool := none
+  /--
+  Additional modules imported for each environment
+  used in running code quality checks.
+  -/
+  checks : Array Name := #[]
 
   /--
   Whether this package is expected to function only on a single toolchain

tests/elab/code_quality_check.lean

@@ -3,30 +3,41 @@ import Lean
 /-!
 Tests the code-quality check framework (`Lean.Linter.CodeQuality`): the
 `package_code_quality_check` attribute, the backing `packageCheckExt` environment extension,
-and the concurrent `runPackageChecks` driver producing a combined entry array. Checks
-receive a `PackageCheckContext` with driver-provided inputs such as the package root.
-A check that throws is reported on stderr and contributes no entries.
+and the concurrent `runPackageChecks` driver producing a combined entry array. Checks run in
+`MetaM` and receive a `PackageCheckContext` with the driver-provided source search path and
+top-level module. A check that throws contributes no entries; its error is collected into
+the result's `errors`.
 -/
 
 open Lean Linter CodeQuality
 
 /-! ## Dummy checks for testing -/
 
 @[package_code_quality_check]
-public meta def dummyMetric : PackageCheck := fun _ =>
-  return #[
-    { name := "dummyMetric", source := .module `MyModule, value := .scalar 42.0 },
-    { name := "dummyMetric", source := .declaration `MyModule `MyModule.foo, value := .scalar 1.0 }]
+public meta def dummyMetric : PackageCheck where
+  run _ :=
+    return #[
+      { name := "dummyMetric", source := .module `MyModule, value := .scalar 42.0 },
+      { name := "dummyMetric", source := .declaration `MyModule `MyModule.foo, value := .scalar 1.0 }]
 
 @[package_code_quality_check]
-public meta def dictMetric : PackageCheck := fun _ =>
-  return #[
+public meta def dictMetric : PackageCheck where
+  run _ := return #[
     { name := "dictMetric", source := .module `MyModule,
       value := .dict (Std.TreeMap.empty.insert "a" 1.0 |>.insert "b" 2.0) }]
 
 @[package_code_quality_check]
-public meta def pkgRootMetric : PackageCheck := fun ctx =>
-  return #[{ name := "pkgRootMetric", source := .module ctx.pkgRoot, value := .scalar 0.0 }]
+public meta def pkgRootMetric : PackageCheck where
+  run _ :=
+    return #[{ name := "pkgRootMetric", source := .declaration `hello `world , value := .scalar 0.0 }]
+
+-- Reports on the context's top-level module and reads the environment, exercising both the
+-- `topLevelModule` input and the `MetaM` interface of a check.
+@[package_code_quality_check]
+public meta def topLevelMetric : PackageCheck where
+  run ctx := do
+    let hasNat := if (← getEnv).contains ``Nat then 1.0 else 0.0
+    return #[{ name := "topLevelMetric", source := .module ctx.topLevelModule, value := .scalar hasNat }]
 
 /-! ## Test: the extension tracks registered checks -/
 
@@ -46,32 +57,40 @@ def testExtContains (name : Name) : CoreM Bool := do
 def testGetPackageChecks : CoreM (Array Name) := do
   return (← getPackageChecks).map (·.declName)
 
-/-- info: #[`dummyMetric, `dictMetric, `pkgRootMetric] -/
+/-- info: #[`dictMetric, `dummyMetric, `pkgRootMetric, `topLevelMetric] -/
 #guard_msgs in
 #eval testGetPackageChecks
 
 /-! ## Test: runPackageChecks combines all results into one entry array, threading the context -/
 
 def testRunPackageChecks : CoreM String := do
-  let entries ← runPackageChecks (← getPackageChecks) { pkgRoot := `MyPkg }
+  let ⟨entries, _⟩ ← runPackageChecks (← getPackageChecks)
+    { srcSearchPath := [], topLevelModule := `MyTopLevel }
   return (toJson entries).compress
 
+def testRunPackageErrors : CoreM (Array String) := do
+  let ⟨_, errors⟩ ← runPackageChecks (← getPackageChecks)
+    { srcSearchPath := [], topLevelModule := `MyTopLevel }
+  errors.mapM (·.toString)
+
 /--
-info: "[{\"name\":\"dummyMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"scalar\":{\"value\":42}}},{\"name\":\"dummyMetric\",\"source\":{\"declaration\":{\"module\":\"MyModule\",\"name\":\"MyModule.foo\"}},\"value\":{\"scalar\":{\"value\":1}}},{\"name\":\"dictMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"dict\":{\"dictionary\":{\"a\":1,\"b\":2}}}},{\"name\":\"pkgRootMetric\",\"source\":{\"module\":{\"name\":\"MyPkg\"}},\"value\":{\"scalar\":{\"value\":0}}}]"
+info: "[{\"name\":\"dictMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"dict\":{\"dictionary\":{\"a\":1,\"b\":2}}}},{\"name\":\"dummyMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"scalar\":{\"value\":42}}},{\"name\":\"dummyMetric\",\"source\":{\"declaration\":{\"module\":\"MyModule\",\"name\":\"MyModule.foo\"}},\"value\":{\"scalar\":{\"value\":1}}},{\"name\":\"pkgRootMetric\",\"source\":{\"declaration\":{\"module\":\"hello\",\"name\":\"world\"}},\"value\":{\"scalar\":{\"value\":0}}},{\"name\":\"topLevelMetric\",\"source\":{\"module\":{\"name\":\"MyTopLevel\"}},\"value\":{\"scalar\":{\"value\":1}}}]"
 -/
 #guard_msgs in
 #eval testRunPackageChecks
 
 /-! ## Test: a failing check is reported on stderr and skipped; other checks still run -/
 
 @[package_code_quality_check]
-public meta def failingMetric : PackageCheck := fun _ =>
-  throwError "boom"
+public meta def failingMetric : PackageCheck where
+  run _ := throwError "boom"
+
+/-- info: #["failingMetric has failed: boom"] -/
+#guard_msgs in
+#eval testRunPackageErrors
 
 /--
-info: code quality check `failingMetric` failed: boom
----
-info: "[{\"name\":\"dummyMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"scalar\":{\"value\":42}}},{\"name\":\"dummyMetric\",\"source\":{\"declaration\":{\"module\":\"MyModule\",\"name\":\"MyModule.foo\"}},\"value\":{\"scalar\":{\"value\":1}}},{\"name\":\"dictMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"dict\":{\"dictionary\":{\"a\":1,\"b\":2}}}},{\"name\":\"pkgRootMetric\",\"source\":{\"module\":{\"name\":\"MyPkg\"}},\"value\":{\"scalar\":{\"value\":0}}}]"
+info: "[{\"name\":\"dictMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"dict\":{\"dictionary\":{\"a\":1,\"b\":2}}}},{\"name\":\"dummyMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}},\"value\":{\"scalar\":{\"value\":42}}},{\"name\":\"dummyMetric\",\"source\":{\"declaration\":{\"module\":\"MyModule\",\"name\":\"MyModule.foo\"}},\"value\":{\"scalar\":{\"value\":1}}},{\"name\":\"pkgRootMetric\",\"source\":{\"declaration\":{\"module\":\"hello\",\"name\":\"world\"}},\"value\":{\"scalar\":{\"value\":0}}},{\"name\":\"topLevelMetric\",\"source\":{\"module\":{\"name\":\"MyTopLevel\"}},\"value\":{\"scalar\":{\"value\":1}}}]"
 -/
 #guard_msgs in
 #eval testRunPackageChecks
@@ -82,7 +101,8 @@ info: "[{\"name\":\"dummyMetric\",\"source\":{\"module\":{\"name\":\"MyModule\"}
 error: invalid attribute `package_code_quality_check`, declaration `notMeta` must be marked as `public` and `meta` but is only marked `public`
 -/
 #guard_msgs in
-@[package_code_quality_check] public def notMeta : PackageCheck := fun _ => return #[]
+@[package_code_quality_check] public def notMeta : PackageCheck where
+  run _ := return #[]
 
 /-! ## Test: a declaration of the wrong type is rejected -/