From ca1cbaa6e9692ffc8d5694eb841df9578e7ecf76 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 28 Mar 2024 23:19:46 -0400 Subject: [PATCH] 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 | 12 +++++++++ src/lake/Lake/CLI/Help.lean | 11 ++++++++ src/lake/Lake/CLI/Main.lean | 16 +++++++++++ src/lake/Lake/CLI/Translate/Lean.lean | 26 +++++++++++------- src/lake/Lake/CLI/Translate/Toml.lean | 1 + src/lake/Lake/Config/Package.lean | 2 ++ src/lake/Lake/DSL/Attributes.lean | 9 +++++++ src/lake/Lake/Load/Elab.lean | 1 + src/lake/Lake/Load/Package.lean | 10 ++++++- src/lake/Lake/Load/Toml.lean | 6 +++-- src/lake/tests/test/clean.sh | 1 + src/lake/tests/test/exe.lean | 7 +++++ src/lake/tests/test/exe.toml | 5 ++++ src/lake/tests/test/none.lean | 4 +++ src/lake/tests/test/none.toml | 1 + src/lake/tests/test/script.lean | 9 +++++++ src/lake/tests/test/test.lean | 2 ++ src/lake/tests/test/test.sh | 27 +++++++++++++++++++ src/lake/tests/test/two.lean | 10 +++++++ .../tests/translateConfig/out.expected.lean | 4 +-- .../tests/translateConfig/out.expected.toml | 3 ++- src/lake/tests/translateConfig/source.lean | 3 ++- src/lake/tests/translateConfig/source.toml | 3 ++- 23 files changed, 155 insertions(+), 18 deletions(-) create mode 100755 src/lake/tests/test/clean.sh create mode 100644 src/lake/tests/test/exe.lean create mode 100644 src/lake/tests/test/exe.toml create mode 100644 src/lake/tests/test/none.lean create mode 100644 src/lake/tests/test/none.toml create mode 100644 src/lake/tests/test/script.lean create mode 100644 src/lake/tests/test/test.lean create mode 100755 src/lake/tests/test/test.sh create mode 100644 src/lake/tests/test/two.lean diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean index 3ef604a9f9..30fae026a9 100644 --- a/src/lake/Lake/CLI/Actions.lean +++ b/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}`" diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 6729f43995..bff934a2db 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -18,6 +18,7 @@ COMMANDS: init create a Lean package in the current directory build ... build targets exe ... build an exe and run it in Lake's environment + test run the workspace's test script or executable clean remove build outputs env ... 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 [-- ...] + +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 diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index b993a7bf28..e82c57e882 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 242fe17c27..0adb7226e2 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/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) diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean index d1a70f7aae..6d0b537da7 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/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 diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index ec04c7530e..f76a5fbada 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/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 diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean index 2d2af9a4d5..0809b1fc33 100644 --- a/src/lake/Lake/DSL/Attributes.lean +++ b/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" diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean index c1ba7e5467..af1ccc1b09 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/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 diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 0a2f01647c..5b698e1ef8 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/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 } diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 876d941131..413092e0ba 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/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 diff --git a/src/lake/tests/test/clean.sh b/src/lake/tests/test/clean.sh new file mode 100755 index 0000000000..b6e54c681e --- /dev/null +++ b/src/lake/tests/test/clean.sh @@ -0,0 +1 @@ +rm -rf .lake lake-manifest.json diff --git a/src/lake/tests/test/exe.lean b/src/lake/tests/test/exe.lean new file mode 100644 index 0000000000..59a2f3fbcd --- /dev/null +++ b/src/lake/tests/test/exe.lean @@ -0,0 +1,7 @@ +import Lake +open System Lake DSL + +package test + +@[test_runner] +lean_exe test diff --git a/src/lake/tests/test/exe.toml b/src/lake/tests/test/exe.toml new file mode 100644 index 0000000000..e1f3289bdc --- /dev/null +++ b/src/lake/tests/test/exe.toml @@ -0,0 +1,5 @@ +name = "test" +testRunner = "test" + +[[lean_exe]] +name = "test" diff --git a/src/lake/tests/test/none.lean b/src/lake/tests/test/none.lean new file mode 100644 index 0000000000..82cb14f82c --- /dev/null +++ b/src/lake/tests/test/none.lean @@ -0,0 +1,4 @@ +import Lake +open System Lake DSL + +package test diff --git a/src/lake/tests/test/none.toml b/src/lake/tests/test/none.toml new file mode 100644 index 0000000000..bc51eed841 --- /dev/null +++ b/src/lake/tests/test/none.toml @@ -0,0 +1 @@ +name = "test" diff --git a/src/lake/tests/test/script.lean b/src/lake/tests/test/script.lean new file mode 100644 index 0000000000..d6ce2585f0 --- /dev/null +++ b/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 diff --git a/src/lake/tests/test/test.lean b/src/lake/tests/test/test.lean new file mode 100644 index 0000000000..cbbcfcdf8c --- /dev/null +++ b/src/lake/tests/test/test.lean @@ -0,0 +1,2 @@ +def main (args : List String) : IO PUnit := do + IO.println s!"exe: {args}" diff --git a/src/lake/tests/test/test.sh b/src/lake/tests/test/test.sh new file mode 100755 index 0000000000..1e0d1b7fca --- /dev/null +++ b/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) diff --git a/src/lake/tests/test/two.lean b/src/lake/tests/test/two.lean new file mode 100644 index 0000000000..28cd7dd01b --- /dev/null +++ b/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 diff --git a/src/lake/tests/translateConfig/out.expected.lean b/src/lake/tests/translateConfig/out.expected.lean index 9e8159ea7f..86d105d738 100644 --- a/src/lake/tests/translateConfig/out.expected.lean +++ b/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 diff --git a/src/lake/tests/translateConfig/out.expected.toml b/src/lake/tests/translateConfig/out.expected.toml index 8706c1391c..89b532b4a7 100644 --- a/src/lake/tests/translateConfig/out.expected.toml +++ b/src/lake/tests/translateConfig/out.expected.toml @@ -1,5 +1,6 @@ name = "test" -defaultTargets = ["b"] +testRunner = "b" +defaultTargets = ["A"] [[require]] name = "foo" diff --git a/src/lake/tests/translateConfig/source.lean b/src/lake/tests/translateConfig/source.lean index 6ede4aae71..83c74f58c3 100644 --- a/src/lake/tests/translateConfig/source.lean +++ b/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 diff --git a/src/lake/tests/translateConfig/source.toml b/src/lake/tests/translateConfig/source.toml index 07d1cefeb6..d190465c35 100644 --- a/src/lake/tests/translateConfig/source.toml +++ b/src/lake/tests/translateConfig/source.toml @@ -1,4 +1,5 @@ -defaultTargets = ['b'] +testRunner = "b" +defaultTargets = ['A'] name = "test" extraDepTargets = []