feat: lake test

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 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}: package has no script or executable tagged `@[test_runner]`"
+  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
@@ -131,6 +132,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
 
@@ -256,6 +266,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

@@ -319,6 +319,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 := test ws.root 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)
@@ -392,6 +406,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/Config/Package.lean

@@ -201,6 +201,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

@@ -106,6 +106,14 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
       else
         error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`"
     | .error e => error e
+  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
@@ -117,7 +125,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
   return {self with
     opaqueDeps := deps.map (.mk ·)
     leanLibConfigs, leanExeConfigs, externLibConfigs
-    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts,
+    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts, testRunner
     postUpdateHooks
   }
 

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/exe.lean

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

src/lake/tests/test/none.lean

@@ -0,0 +1,4 @@
+import Lake
+open System Lake DSL
+
+package 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.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+# Script test runner
+$LAKE -f script.lean test | grep -F "script: []"
+$LAKE -f script.lean test -- hello | grep --color "hello"
+
+# Executable test runner
+$LAKE -f exe.lean test | grep -F "exe: []"
+$LAKE -f exe.lean 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 "package has no"
+
+# Test runner checker
+$LAKE -f exe.lean check-test
+$LAKE -f script.lean check-test
+($LAKE -f none.lean check-test && false || true)
+($LAKE -f two.lean 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