feat: lake test improvements & lake lint (#4261)

Extends the functionality of `lake test` and adds a parallel command in
`lake lint`.

* Rename `@[test_runner]` / `testRunner` to `@[test_driver]` /
`testDriver`. The old names are kept as deprecated aliases.
* Extend help page for `lake test` and adds one for `lake check-test`. 
* Add `lake lint` and its parallel tag `@[lint_driver]` , setting
`lintDriver`, and checker `lake check-lint`.
* Add support for specifying test / lint drivers from dependencies. 
* Add `testDriverArgs` / `lintDriverArgs` for fixing additional
arguments to the invocation of a driver script or executable.
* Add support for library test drivers (but not library lint drivers). 
* `lake check-test` / `lake check-lint` only load the package (without
dependencies), not the whole workspace.

Closes #4116. Closes #4121. Closes #4142.

Author: tydeu

src/lake/Lake/CLI/Actions.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Build.Run
 import Lake.Build.Targets
+import Lake.CLI.Build
 
 namespace Lake
 
@@ -28,14 +29,52 @@ def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
   logInfo s!"uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
 
+def Package.resolveDriver
+  (pkg : Package) (kind : String) (driver : String)
+: LakeT IO (Package × String) := do
+  let pkgName := pkg.name.toString (escape := false)
+  if driver.isEmpty then
+    error s!"{pkgName}: no {kind} driver configured"
+  else
+    match driver.split (· == '/') with
+    | [pkg, driver] =>
+      let some pkg ← findPackage? pkg.toName
+        | error s!"{pkgName}: unknown {kind} driver package '{pkg}'"
+      return (pkg, driver)
+    | [driver] =>
+      return (pkg, driver)
+    | _ =>
+      error s!"{pkgName}: invalid {kind} driver '{driver}' (too many '/')"
+
 def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
+  let cfgArgs := pkg.testDriverArgs
+  let (pkg, driver) ← pkg.resolveDriver "test" pkg.testDriver
   let pkgName := pkg.name.toString (escape := false)
-  if pkg.testRunner.isAnonymous then
-    error s!"{pkgName}: no test runner script or executable"
-  else if let some script := pkg.scripts.find? pkg.testRunner then
-    script.run args
-  else if let some exe := pkg.findLeanExe? pkg.testRunner then
+  if let some script := pkg.scripts.find? driver.toName then
+    script.run (cfgArgs.toList ++ args)
+  else if let some exe := pkg.findLeanExe? driver.toName  then
+    let exeFile ← runBuild exe.fetch buildConfig
+    env exeFile.toString (cfgArgs ++ args.toArray)
+  else if let some lib := pkg.findLeanLib? driver.toName then
+    unless cfgArgs.isEmpty ∧ args.isEmpty do
+      error s!"{pkgName}: arguments cannot be passed to a library test driver"
+    match resolveLibTarget (← getWorkspace) lib with
+    | .ok specs =>
+      runBuild (buildSpecs specs) {buildConfig with out := .stdout}
+      return 0
+    | .error e =>
+      error s!"{pkgName}: invalid test driver: {e}"
+  else
+    error s!"{pkgName}: invalid test driver: unknown script, executable, or library '{driver}'"
+
+def Package.lint (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
+  let cfgArgs := pkg.lintDriverArgs
+  let (pkg, driver) ← pkg.resolveDriver "lint" pkg.lintDriver
+  if let some script := pkg.scripts.find? driver.toName then
+    script.run (cfgArgs.data ++ args)
+  else if let some exe := pkg.findLeanExe? driver.toName  then
     let exeFile ← runBuild exe.fetch buildConfig
-    env exeFile.toString args.toArray
+    env exeFile.toString (cfgArgs ++ args.toArray)
   else
-    error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`"
+    let pkgName := pkg.name.toString (escape := false)
+    error s!"{pkgName}: invalid lint driver: unknown script or executable '{driver}'"

src/lake/Lake/CLI/Build.lean

@@ -15,15 +15,18 @@ structure BuildSpec where
   getBuildJob : BuildData info.key → BuildJob Unit
 
 @[inline] def BuildData.toBuildJob
-[FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit :=
+  [FamilyOut BuildData k (BuildJob α)] (data : BuildData k)
+: BuildJob Unit :=
   discard <| ofFamily data
 
-@[inline] def mkBuildSpec (info : BuildInfo)
-[FamilyOut BuildData info.key (BuildJob α)] : BuildSpec :=
+@[inline] def mkBuildSpec
+  (info : BuildInfo) [FamilyOut BuildData info.key (BuildJob α)]
+: BuildSpec :=
   {info, getBuildJob := BuildData.toBuildJob}
 
-@[inline] def mkConfigBuildSpec (facetType : String)
-(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+@[inline] def mkConfigBuildSpec
+  (facetType : String) (info : BuildInfo)
+  (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
 : Except CliError BuildSpec := do
   let some getJob := config.getJob?
     | throw <| CliError.nonCliFacet facetType facet
@@ -47,15 +50,19 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
     | none => throw <| CliError.unknownPackage spec
 
 open Module in
-def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec :=
+def resolveModuleTarget
+  (ws : Workspace) (mod : Module) (facet : Name := .anonymous)
+: Except CliError BuildSpec :=
   if facet.isAnonymous then
     return mkBuildSpec <| mod.facet leanArtsFacet
   else if let some config := ws.findModuleFacetConfig? facet then do
     mkConfigBuildSpec "module" (mod.facet facet) config rfl
   else
     throw <| CliError.unknownFacet "module" facet
 
-def resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Name) : Except CliError (Array BuildSpec) :=
+def resolveLibTarget
+  (ws : Workspace) (lib : LeanLib) (facet : Name := .anonymous)
+: Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then
     lib.defaultFacets.mapM (resolveFacet ·)
   else

src/lake/Lake/CLI/Help.lean

@@ -18,7 +18,10 @@ COMMANDS:
   init <name> <temp>    create a Lean package in the current directory
   build <targets>...    build targets
   exe <exe> <args>...   build an exe and run it in Lake's environment
-  test                  run the workspace's test script or executable
+  test                  test the package using the configured test driver
+  check-test            check if there is a properly configured test driver
+  lint                  lint the package using the configured lint driver
+  check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
@@ -142,13 +145,62 @@ of the same package, the version materialized is undefined.
 A bare `lake update` will upgrade all dependencies."
 
 def helpTest :=
-"Run the workspace's test script or executable
+"Test the workspace's root package using its configured test driver
 
 USAGE:
   lake test [-- <args>...]
 
-Looks for a script or executable tagged `@[test_runner]` in the workspace's
-root package and executes it with `args`. "
+A test driver can be configured by either setting the 'testDriver'
+package configuration option or by tagging a script, executable, or library
+`@[test_driver]`. A definition in a dependency can be used as a test driver
+by using the `<pkg>/<name>` syntax for the 'testDriver' configuration option.
+
+A script test driver will be run with the  package configuration's
+`testDriverArgs` plus the CLI `args`. An executable test driver will be
+built and then run like a script. A library test driver will just be built.
+"
+
+def helpCheckTest :=
+"Check if there is a properly configured test driver
+
+USAGE:
+  lake check-test
+
+Exits with code 0 if the workspace's root package has a properly
+configured lint driver. Errors (with code 1) otherwise.
+
+Does NOT verify that the configured test driver actually exists in the
+package or its dependencies. It merely verifies that one is specified.
+"
+
+def helpLint :=
+"Lint the workspace's root package using its configured lint driver
+
+USAGE:
+  lake lint [-- <args>...]
+
+A lint driver can be configured by either setting the `lintDriver` package
+configuration option by tagging a script or executable `@[lint_driver]`.
+A definition in dependency can be used as a test driver by using the
+`<pkg>/<name>` syntax for the 'testDriver' configuration option.
+
+A script lint driver will be run with the  package configuration's
+`lintDriverArgs` plus the CLI `args`. An executable lint driver will be
+built and then run like a script.
+"
+
+def helpCheckLint :=
+"Check if there is a properly configured lint driver
+
+USAGE:
+  lake check-lint
+
+Exits with code 0 if the workspace's root package has a properly
+configured lint driver. Errors (with code 1) otherwise.
+
+Does NOT verify that the configured lint driver actually exists in the
+package or its dependencies. It merely verifies that one is specified.
+"
 
 def helpUpload :=
 "Upload build artifacts to a GitHub release
@@ -302,6 +354,9 @@ def help : (cmd : String) → String
 | "update" | "upgrade"  => helpUpdate
 | "upload"              => helpUpload
 | "test"                => helpTest
+| "check-test"          => helpCheckTest
+| "lint"                => helpLint
+| "check-lint"          => helpCheckLint
 | "clean"               => helpClean
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList

src/lake/Lake/CLI/Main.lean

@@ -346,16 +346,28 @@ protected def setupFile : CliM PUnit := do
 protected def test : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let config ← mkLoadConfig opts
-  let ws ← loadWorkspace config
+  let ws ← loadWorkspace (← mkLoadConfig opts)
   noArgsRem do
   let x := ws.root.test opts.subArgs (mkBuildConfig opts)
   exit <| ← x.run (mkLakeContext ws)
 
 protected def checkTest : CliM PUnit := do
   processOptions lakeOption
-  let ws ← loadWorkspace ( ← mkLoadConfig (← getThe LakeOptions))
-  noArgsRem do exit <| if ws.root.testRunner.isAnonymous then 1 else 0
+  let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if pkg.testDriver.isEmpty then 1 else 0
+
+protected def lint : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let ws ← loadWorkspace (← mkLoadConfig opts)
+  noArgsRem do
+  let x := ws.root.lint opts.subArgs (mkBuildConfig opts)
+  exit <| ← x.run (mkLakeContext ws)
+
+protected def checkLint : CliM PUnit := do
+  processOptions lakeOption
+  let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if pkg.lintDriver.isEmpty then 1 else 0
 
 protected def clean : CliM PUnit := do
   processOptions lakeOption
@@ -440,8 +452,7 @@ protected def translateConfig : CliM PUnit := do
   let lang ← parseLangSpec (← takeArg "configuration language")
   let outFile? := (← takeArg?).map FilePath.mk
   noArgsRem do
-  Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
-  let (pkg, _) ← loadPackage "[root]" cfg
+  let pkg ← loadPackage cfg
   let outFile := outFile?.getD <| pkg.configFile.withExtension lang.fileExtension
   if (← outFile.pathExists) then
     throw (.outputConfigExists outFile)
@@ -468,6 +479,8 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "setup-file"          => lake.setupFile
 | "test"                => lake.test
 | "check-test"          => lake.checkTest
+| "lint"                => lake.lint
+| "check-lint"          => lake.checkLint
 | "clean"               => lake.clean
 | "script"              => lake.script
 | "scripts"             => lake.script.list

src/lake/Lake/CLI/Translate/Lean.lean

@@ -89,8 +89,10 @@ def LeanConfig.addDeclFields (cfg : LeanConfig) (fs : Array DeclField) : Array D
 @[inline] def mkDeclValWhere? (fields : Array DeclField) : Option (TSyntax ``declValWhere) :=
   if fields.isEmpty then none else Unhygienic.run `(declValWhere|where $fields*)
 
-def PackageConfig.mkSyntax (cfg : PackageConfig) : PackageDecl := Unhygienic.run do
-  let declVal? := mkDeclValWhere? <|Array.empty
+def PackageConfig.mkSyntax (cfg : PackageConfig)
+  (testDriver := cfg.testDriver) (lintDriver := cfg.lintDriver)
+  : PackageDecl := Unhygienic.run do
+  let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `precompileModules cfg.precompileModules false
     |> addDeclFieldD `moreGlobalServerArgs cfg.moreGlobalServerArgs #[]
     |> addDeclFieldD `srcDir cfg.srcDir "."
@@ -102,6 +104,10 @@ def PackageConfig.mkSyntax (cfg : PackageConfig) : PackageDecl := Unhygienic.run
     |> addDeclField? `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
     |> addDeclFieldD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
     |> addDeclFieldD `preferReleaseBuild cfg.preferReleaseBuild false
+    |> addDeclFieldD `testDriver testDriver ""
+    |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
+    |> addDeclFieldD `lintDriver lintDriver ""
+    |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
     |> cfg.toWorkspaceConfig.addDeclFields
     |> cfg.toLeanConfig.addDeclFields
   `(packageDecl|package $(mkIdent cfg.name) $[$declVal?]?)
@@ -145,19 +151,15 @@ protected def LeanLibConfig.mkSyntax
   `(leanLibDecl|$[$attrs?:attributes]? lean_lib $(mkIdent cfg.name) $[$declVal?]?)
 
 protected def LeanExeConfig.mkSyntax
-  (cfg : LeanExeConfig) (defaultTarget := false) (testRunner := false)
+  (cfg : LeanExeConfig) (defaultTarget := false)
 : LeanExeDecl := Unhygienic.run do
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `srcDir cfg.srcDir "."
     |> addDeclFieldD `root cfg.root cfg.name
     |> addDeclFieldD `exeName cfg.exeName (cfg.name.toStringWithSep "-" (escape := false))
     |> addDeclFieldD `supportInterpreter cfg.supportInterpreter false
     |> cfg.toLeanConfig.addDeclFields
-  let attrs? ← id do
-    let mut attrs := #[]
-    if testRunner then attrs := attrs.push <| ← `(Term.attrInstance|test_runner)
-    if defaultTarget then attrs := attrs.push <| ← `(Term.attrInstance|default_target)
-    if attrs.isEmpty then pure none else some <$> `(Term.attributes|@[$attrs,*])
+    let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
   `(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name) $[$declVal?]?)
 
 protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
@@ -175,14 +177,13 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic
 
 /-- Create a Lean module that encodes the declarative configuration of the package. -/
 def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
-  let testRunner := pkg.testRunner
   let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
-  let pkgConfig := pkg.config.mkSyntax
+  let pkgConfig := pkg.config.mkSyntax pkg.testDriver pkg.lintDriver
   let requires := pkg.depConfigs.map (·.mkSyntax)
   let leanLibs := pkg.leanLibConfigs.toArray.map fun cfg =>
     cfg.mkSyntax (defaultTargets.contains cfg.name)
   let leanExes := pkg.leanExeConfigs.toArray.map fun cfg =>
-    cfg.mkSyntax (defaultTargets.contains cfg.name) (cfg.name == testRunner)
+    cfg.mkSyntax (defaultTargets.contains cfg.name)
   `(module|
   import $(mkIdent `Lake)
   open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)

src/lake/Lake/CLI/Translate/Toml.lean

@@ -122,7 +122,10 @@ instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩
 /-- Create a TOML table that encodes the declarative configuration of the package. -/
 def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
   pkg.config.toToml t
-  |>.insertD `testRunner pkg.testRunner .anonymous
+  |>.smartInsert `testDriver pkg.testDriver
+  |>.smartInsert `testDriverArgs pkg.testDriverArgs
+  |>.smartInsert `lintDriver pkg.lintDriver
+  |>.smartInsert `lintDriverArgs pkg.lintDriverArgs
   |>.smartInsert `defaultTargets pkg.defaultTargets
   |>.smartInsert `require pkg.depConfigs
   |>.smartInsert `lean_lib pkg.leanLibConfigs.toArray