feat: lake test (#3779)

Adds a `lake test` CLI command that runs a `script` or `lean_exe` tagged
`@[test_runner]` in the workspace's root package.

src/lake/Lake/CLI/Actions.lean

@@ -26,3 +26,15 @@ def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
   tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile
   logInfo s!"Uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
+
+def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT LogIO UInt32 := do
+  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
+    let exeFile ← runBuild (exe.build >>= (·.await)) buildConfig
+    env exeFile.toString args.toArray
+  else
+    error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`"

src/lake/Lake/CLI/Help.lean

@@ -18,6 +18,7 @@ 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
   clean                 remove build outputs
   env <cmd> <args>...   execute a command in Lake's environment
   update                update dependencies and save them to the manifest
@@ -135,6 +136,15 @@ 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
+
+USAGE:
+  lake test [-- <args>...]
+
+Looks for a script or executable tagged `@[test_runner]` in the workspace's
+root package and executes it with `args`. "
+
 def helpUpload :=
 "Upload build artifacts to a GitHub release
 
@@ -275,6 +285,7 @@ def help : (cmd : String) → String
 | "build"               => helpBuild
 | "update" | "upgrade"  => helpUpdate
 | "upload"              => helpUpload
+| "test"                => helpTest
 | "clean"               => helpClean
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList

src/lake/Lake/CLI/Main.lean

@@ -335,6 +335,20 @@ protected def setupFile : CliM PUnit := do
   let imports ← takeArgs
   setupFile loadConfig filePath imports buildConfig opts.verbosity
 
+protected def test : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  noArgsRem do
+  let x := ws.root.test opts.subArgs (mkBuildConfig opts)
+  exit <| ← x.run (mkLakeContext ws) |>.run (MonadLog.io opts.verbosity)
+
+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
+
 protected def clean : CliM PUnit := do
   processOptions lakeOption
   let config ← mkLoadConfig (← getThe LakeOptions)
@@ -424,6 +438,8 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "resolve-deps"        => lake.resolveDeps
 | "upload"              => lake.upload
 | "setup-file"          => lake.setupFile
+| "test"                => lake.test
+| "check-test"          => lake.checkTest
 | "clean"               => lake.clean
 | "script"              => lake.script
 | "scripts"             => lake.script.list

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

@@ -130,10 +130,9 @@ protected def Glob.quote (glob : Glob) : Term := Unhygienic.run do
 
 local instance : Quote Glob := ⟨Glob.quote⟩
 
-@[inline] private def mkConfigAttrs? (defaultTarget : Bool) : Option Attributes :=
-  if defaultTarget then Unhygienic.run `(Term.attributes|@[default_target]) else none
-
-protected def LeanLibConfig.mkSyntax (cfg : LeanLibConfig) (defaultTarget := false) : LeanLibDecl := Unhygienic.run do
+protected def LeanLibConfig.mkSyntax
+  (cfg : LeanLibConfig) (defaultTarget := false)
+: LeanLibDecl := Unhygienic.run do
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `srcDir cfg.srcDir "."
     |> addDeclFieldD `roots cfg.roots #[cfg.name]
@@ -142,20 +141,26 @@ protected def LeanLibConfig.mkSyntax (cfg : LeanLibConfig) (defaultTarget := fal
     |> addDeclFieldD `precompileModules cfg.precompileModules false
     |> addDeclFieldD `defaultFacets cfg.defaultFacets #[LeanLib.leanArtsFacet]
     |> cfg.toLeanConfig.addDeclFields
-  let attrs? := mkConfigAttrs? defaultTarget
+  let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
   `(leanLibDecl|$[$attrs?:attributes]? lean_lib $(mkIdent cfg.name) $[$declVal?]?)
 
-protected def LeanExeConfig.mkSyntax (cfg : LeanExeConfig) (defaultTarget := false) : LeanExeDecl := Unhygienic.run do
+protected def LeanExeConfig.mkSyntax
+  (cfg : LeanExeConfig) (defaultTarget := false) (testRunner := 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? := mkConfigAttrs? defaultTarget
+  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,*])
   `(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name) $[$declVal?]?)
 
-protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl:= Unhygienic.run do
+protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
   let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
     cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>
       `($stx |>.insert $(quote opt) $(quote val))
@@ -170,13 +175,14 @@ 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 pkgConfig := pkg.config.mkSyntax
+  let testRunner := pkg.testRunner
   let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
+  let pkgConfig := pkg.config.mkSyntax
   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.mkSyntax (defaultTargets.contains cfg.name) (cfg.name == testRunner)
   `(module|
   import $(mkIdent `Lake)
   open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)

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

@@ -122,6 +122,7 @@ 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 `defaultTargets pkg.defaultTargets
   |>.smartInsert `require pkg.depConfigs
   |>.smartInsert `lean_lib pkg.leanLibConfigs.toArray

src/lake/Lake/Config/Package.lean

@@ -203,6 +203,8 @@ structure Package where
   defaultScripts : Array Script := #[]
   /-- Post-`lake update` hooks for the package. -/
   postUpdateHooks : Array (OpaquePostUpdateHook config.name) := #[]
+  /-- Name of the package's test runner script or executable (if any). -/
+  testRunner : Name := .anonymous
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance

src/lake/Lake/DSL/Attributes.lean

@@ -49,6 +49,15 @@ initialize defaultTargetAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
+initialize testRunnerAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `test_runner "mark a Lake script or executable as the package's test runner"
+    fun name => do
+      let valid ← getEnv <&> fun env =>
+        scriptAttr.hasTag env name ||
+        leanExeAttr.hasTag env name
+      unless valid do
+        throwError "attribute `test_runner` can only be used on a `script` or `lean_exe`"
+
 initialize moduleFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
 

src/lake/Lake/Load/Elab.lean

@@ -133,6 +133,7 @@ where
     |>.insert ``externLibAttr
     |>.insert ``targetAttr
     |>.insert ``defaultTargetAttr
+    |>.insert ``testRunnerAttr
     |>.insert ``moduleFacetAttr
     |>.insert ``packageFacetAttr
     |>.insert ``libraryFacetAttr

src/lake/Lake/Load/Package.lean

@@ -109,6 +109,14 @@ def Package.loadFromEnv
     | .error e => error e
   let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
     evalConstCheck env opts Dependency ``Dependency name
+  let testRunners := testRunnerAttr.getAllEntries env
+  let testRunner ←
+    if testRunners.size > 1 then
+      error s!"{self.name}: only one script or executable can be tagged `@[test_runner]`"
+    else if h : testRunners.size > 0 then
+      pure (testRunners[0]'h)
+    else
+      pure .anonymous
 
   -- Deprecation warnings
   unless self.config.manifestFile.isNone do
@@ -119,7 +127,7 @@ def Package.loadFromEnv
   -- Fill in the Package
   return {self with
     depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs
-    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts
+    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts, testRunner
     postUpdateHooks
   }
 

src/lake/Lake/Load/Toml.lean

@@ -259,10 +259,12 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
       let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[]
       let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[]
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
+      let testRunner ← table.tryDecodeD `testRunner .anonymous
       let depConfigs ← table.tryDecodeD `require #[]
       return {
-        dir, relDir, relConfigFile,
-        config, depConfigs, leanLibConfigs, leanExeConfigs, defaultTargets
+        dir, relDir, relConfigFile
+        config, depConfigs, leanLibConfigs, leanExeConfigs
+        defaultTargets, testRunner
       }
     if errs.isEmpty then
       return pkg

src/lake/tests/test/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/test/exe.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_runner]
+lean_exe test

src/lake/tests/test/exe.toml

@@ -0,0 +1,5 @@
+name = "test"
+testRunner = "test"
+
+[[lean_exe]]
+name = "test"

src/lake/tests/test/none.lean

@@ -0,0 +1,4 @@
+import Lake
+open System Lake DSL
+
+package test

src/lake/tests/test/none.toml

@@ -0,0 +1 @@
+name = "test"

src/lake/tests/test/script.lean

@@ -0,0 +1,9 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_runner]
+script test args do
+  IO.println s!"script: {args}"
+  return 0

src/lake/tests/test/test.lean

@@ -0,0 +1,2 @@
+def main (args : List String) : IO PUnit := do
+  IO.println s!"exe: {args}"

src/lake/tests/test/test.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+# Script test runner
+$LAKE -f script.lean test | grep --color -F "script: []"
+$LAKE -f script.lean test -- hello | grep --color "hello"
+
+# Executable test runner
+$LAKE -f exe.lean test | grep --color -F "exe: []"
+$LAKE -f exe.lean test -- hello | grep --color "hello"
+$LAKE -f exe.toml test | grep --color -F "exe: []"
+$LAKE -f exe.toml test -- hello | grep --color "hello"
+
+# Test runner validation
+($LAKE -f two.lean test 2>&1 && false || true) | grep --color "only one"
+($LAKE -f none.lean test 2>&1 && false || true) | grep --color "no test runner"
+($LAKE -f none.toml test 2>&1 && false || true) | grep --color "no test runner"
+
+# Test runner checker
+$LAKE -f exe.lean check-test
+$LAKE -f exe.toml check-test
+$LAKE -f script.lean check-test
+($LAKE -f two.lean check-test && false || true)
+($LAKE -f none.lean check-test && false || true)
+($LAKE -f none.toml check-test && false || true)

src/lake/tests/test/two.lean

@@ -0,0 +1,10 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_runner]
+lean_exe testExe
+
+@[test_runner]
+script testScript do return 1

src/lake/tests/translateConfig/out.expected.lean

@@ -11,6 +11,6 @@ require foo from "-" with Lake.NameMap.empty |>.insert `foo "bar"
 
 require bar from git "https://example.com"@"abc"/"sub/dir"
 
-lean_lib A
+@[default_target] lean_lib A
 
-@[default_target] lean_exe b
+@[test_runner] lean_exe b

src/lake/tests/translateConfig/out.expected.toml

@@ -1,5 +1,6 @@
 name = "test"
-defaultTargets = ["b"]
+testRunner = "b"
+defaultTargets = ["A"]
 
 [[require]]
 name = "foo"

src/lake/tests/translateConfig/source.lean

@@ -34,6 +34,7 @@ package test where
 require foo from "dir" with NameMap.empty.insert `foo "bar"
 require bar from git "https://example.com" @ "abc" / "sub" / "dir"
 
+@[default_target]
 lean_lib A where
   srcDir := "."
   roots := #[`A]
@@ -44,7 +45,7 @@ lean_lib A where
   nativeFacets := fun _ => #[]
   toLeanConfig := testLeanConfig
 
-@[default_target]
+@[test_runner]
 lean_exe b where
   srcDir := "."
   root := `b

src/lake/tests/translateConfig/source.toml

@@ -1,4 +1,5 @@
-defaultTargets = ['b']
+testRunner = "b"
+defaultTargets = ['A']
 
 name = "test"
 extraDepTargets = []