diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean index 326003c978..83c4c434e5 100644 --- a/src/lake/Lake/CLI/Actions.lean +++ b/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.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do +def Package.resolveDriver + (pkg : Package) (kind : String) (driver : String) +: LakeT IO (Package × String) := 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.fetch buildConfig - env exeFile.toString args.toArray + if driver.isEmpty then + error s!"{pkgName}: no {kind} driver configured" else - error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`" + 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 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 (cfgArgs ++ args.toArray) + else + let pkgName := pkg.name.toString (escape := false) + error s!"{pkgName}: invalid lint driver: unknown script or executable '{driver}'" diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean index dee47451fc..93d2f82bad 100644 --- a/src/lake/Lake/CLI/Build.lean +++ b/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,7 +50,9 @@ 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 @@ -55,7 +60,9 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except 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 diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index cd949306a0..c0efc2ad54 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -18,7 +18,10 @@ 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 + 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 ... execute a command in Lake's environment lean 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 [-- ...] -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 `/` 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 [-- ...] + +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 +`/` 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 diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 326cfa7474..3b4eaaf5ed 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 0adb7226e2..6d71f5ab52 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/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,7 +151,7 @@ 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 "." @@ -153,11 +159,7 @@ protected def LeanExeConfig.mkSyntax |> 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) diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean index 6d0b537da7..952c2590c4 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/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 diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index f76a5fbada..3785a9c531 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -154,6 +154,44 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where -/ preferReleaseBuild : Bool := false + /-- + The name of the script, executable, or library by `lake test` when + this package is the workspace root. To point to a definition in another + package, use the syntax `/`. + + A script driver will be run by `lake test` with the arguments + configured in `testDriverArgs` followed by any specified on the CLI + (e.g., via `lake lint -- ...`). An executable driver will be built + and then run like a script. A library will just be built. + -/ + testDriver : String := "" + + /-- + Arguments to pass to the package's test driver. + These arguments will come before those passed on the command line via + `lake test -- ...`. + -/ + testDriverArgs : Array String := #[] + + /-- + The name of the script or executable used by `lake lint` when this package + is the workspace root. To point to a definition in another package, use the + syntax `/`. + + A script driver will be run by `lake lint` with the arguments + configured in `lintDriverArgs` followed by any specified on the CLI + (e.g., via `lake lint -- ...`). An executable driver will be built + and then run like a script. + -/ + lintDriver : String := "" + + /-- + Arguments to pass to the package's linter. + These arguments will come before those passed on the command line via + `lake lint -- ...`. + -/ + lintDriverArgs : Array String := #[] + deriving Inhabited -------------------------------------------------------------------------------- @@ -203,8 +241,11 @@ 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 + /-- The driver used for `lake test` when this package is the workspace root. -/ + testDriver : String := config.testDriver + /-- The driver used for `lake lint` when this package is the workspace root. -/ + lintDriver : String := config.lintDriver + instance : Nonempty Package := have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance @@ -287,6 +328,14 @@ namespace Package @[inline] def buildDir (self : Package) : FilePath := self.dir / self.config.buildDir +/-- The package's `testDriverArgs` configuration. -/ +@[inline] def testDriverArgs (self : Package) : Array String := + self.config.testDriverArgs + +/-- The package's `lintDriverArgs` configuration. -/ +@[inline] def lintDriverArgs (self : Package) : Array String := + self.config.lintDriverArgs + /-- The package's `extraDepTargets` configuration. -/ @[inline] def extraDepTargets (self : Package) : Array Name := self.config.extraDepTargets diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean index 0809b1fc33..7c89acd56c 100644 --- a/src/lake/Lake/DSL/Attributes.lean +++ b/src/lake/Lake/DSL/Attributes.lean @@ -1,68 +1,22 @@ /- -Copyright (c) 2021 Mac Malone. All rights reserved. +Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lake.Util.OrderedTagAttribute +import Lake.DSL.AttributesCore open Lean + namespace Lake -initialize packageAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `package "mark a definition as a Lake package configuration" - -initialize packageDepAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency" - -initialize postUpdateAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook" - -initialize scriptAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `script "mark a definition as a Lake script" - -initialize defaultScriptAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `default_script "mark a Lake script as the package's default" - fun name => do - unless (← getEnv <&> (scriptAttr.hasTag · name)) do - throwError "attribute `default_script` can only be used on a `script`" - -initialize leanLibAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration" - -initialize leanExeAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration" - -initialize externLibAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target" - -initialize targetAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `target "mark a definition as a custom Lake target" - -initialize defaultTargetAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `default_target "mark a Lake target as the package's default" - fun name => do - let valid ← getEnv <&> fun env => - leanLibAttr.hasTag env name || - leanExeAttr.hasTag env name || - externLibAttr.hasTag env name || - targetAttr.hasTag env name - 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" - -initialize packageFacetAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet" - -initialize libraryFacetAttr : OrderedTagAttribute ← - registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet" +initialize + registerBuiltinAttribute { + ref := by exact decl_name% + name := `test_runner + descr := testDriverAttr.attr.descr + add := fun decl stx attrKind => do + logWarningAt stx "@[test_runner] has been deprecated, use @[test_driver] instead" + testDriverAttr.attr.add decl stx attrKind + applicationTime := testDriverAttr.attr.applicationTime + erase := fun decl => testDriverAttr.attr.erase decl + } diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean new file mode 100644 index 0000000000..ad5a00878c --- /dev/null +++ b/src/lake/Lake/DSL/AttributesCore.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Util.OrderedTagAttribute + +open Lean +namespace Lake + +initialize packageAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `package "mark a definition as a Lake package configuration" + +initialize packageDepAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency" + +initialize postUpdateAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook" + +initialize scriptAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `script "mark a definition as a Lake script" + +initialize defaultScriptAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `default_script "mark a Lake script as the package's default" + fun name => do + unless (← getEnv <&> (scriptAttr.hasTag · name)) do + throwError "attribute `default_script` can only be used on a `script`" + +initialize leanLibAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration" + +initialize leanExeAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration" + +initialize externLibAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target" + +initialize targetAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `target "mark a definition as a custom Lake target" + +initialize defaultTargetAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `default_target "mark a Lake target as the package's default" + fun name => do + let valid ← getEnv <&> fun env => + leanLibAttr.hasTag env name || + leanExeAttr.hasTag env name || + externLibAttr.hasTag env name || + targetAttr.hasTag env name + unless valid do + throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)" + +initialize testDriverAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `test_driver "mark a Lake script, executable, or library as package's test driver" + fun name => do + let valid ← getEnv <&> fun env => + scriptAttr.hasTag env name || + leanExeAttr.hasTag env name || + leanLibAttr.hasTag env name + unless valid do + throwError "attribute `test_driver` can only be used on a `script`, `lean_exe`, or `lean_lib`" + +initialize lintDriverAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `lint_driver "mark a Lake script or executable as package's linter" + fun name => do + let valid ← getEnv <&> fun env => + scriptAttr.hasTag env name || + leanExeAttr.hasTag env name + unless valid do + throwError "attribute `lint_driver` can only be used on a `script` or `lean_exe`" + +initialize moduleFacetAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet" + +initialize packageFacetAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet" + +initialize libraryFacetAttr : OrderedTagAttribute ← + registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet" diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean index e6597d5607..86358388c0 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/src/lake/Lake/Load/Elab.lean @@ -133,7 +133,8 @@ where |>.insert ``externLibAttr |>.insert ``targetAttr |>.insert ``defaultTargetAttr - |>.insert ``testRunnerAttr + |>.insert ``testDriverAttr + |>.insert ``lintDriverAttr |>.insert ``moduleFacetAttr |>.insert ``packageFacetAttr |>.insert ``libraryFacetAttr diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index b1defb98a6..df7d703d61 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -53,7 +53,7 @@ def configFileExists (cfgFile : FilePath) : BaseIO Bool := leanFile.pathExists <||> tomlFile.pathExists /-- Loads a Lake package configuration (either Lean or TOML). -/ -def loadPackage +def loadPackageCore (name : String) (cfg : LoadConfig) : LogIO (Package × Option Environment) := do if let some ext := cfg.relConfigFile.extension then @@ -88,7 +88,7 @@ def loadDepPackage (dep : MaterializedDep) (leanOpts : Options) (reconfigure : Bool) : StateT Workspace LogIO Package := fun ws => do let name := dep.name.toString (escape := false) - let (pkg, env?) ← loadPackage name { + let (pkg, env?) ← loadPackageCore name { lakeEnv := ws.lakeEnv wsDir := ws.dir relPkgDir := dep.relPkgDir @@ -110,7 +110,7 @@ Does not resolve dependencies. -/ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do Lean.searchPathRef.set config.lakeEnv.leanSearchPath - let (root, env?) ← loadPackage "[root]" config + let (root, env?) ← loadPackageCore "[root]" config let ws : Workspace := { root, lakeEnv := config.lakeEnv moduleFacetConfigs := initModuleFacetConfigs @@ -122,6 +122,11 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do else return ws +/-- Loads a Lake package as a single independent object (without dependencies). -/ +def loadPackage (config : LoadConfig) : LogIO Package := do + Lean.searchPathRef.set config.lakeEnv.leanSearchPath + (·.1) <$> loadPackageCore "[root]" config + /-- Recursively visits a package dependency graph, avoiding cycles. -/ private def resolveDepsAcyclic [Monad m] [MonadError m] diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 5b698e1ef8..a536baf906 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/src/lake/Lake/Load/Package.lean @@ -109,14 +109,28 @@ 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) + let testDrivers := testDriverAttr.getAllEntries env + let testDriver ← + if testDrivers.size > 1 then + error s!"{self.name}: only one script, executable, or library can be tagged @[test_driver]" + else if h : testDrivers.size > 0 then + if self.config.testDriver.isEmpty then + pure (testDrivers[0]'h |>.toString) + else + error s!"{self.name}: cannot both set testDriver and use @[test_driver]" else - pure .anonymous + pure self.config.testDriver + let lintDrivers := lintDriverAttr.getAllEntries env + let lintDriver ← + if lintDrivers.size > 1 then + error s!"{self.name}: only one script or executable can be tagged @[linter]" + else if h : lintDrivers.size > 0 then + if self.config.lintDriver.isEmpty then + pure (lintDrivers[0]'h |>.toString) + else + error s!"{self.name}: cannot both set linter and use @[linter]" + else + pure self.config.lintDriver -- Deprecation warnings unless self.config.manifestFile.isNone do @@ -127,8 +141,8 @@ def Package.loadFromEnv -- Fill in the Package return {self with depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs - opaqueTargetConfigs, defaultTargets, scripts, defaultScripts, testRunner - postUpdateHooks + opaqueTargetConfigs, defaultTargets, scripts, defaultScripts + testDriver, lintDriver, postUpdateHooks } /-- diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 098051a047..46854e1e97 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -175,12 +175,19 @@ protected def PackageConfig.decodeToml (t : Table) (ref := Syntax.missing) : Exc let releaseRepo ← t.tryDecode? `releaseRepo let buildArchive? ← t.tryDecode? `buildArchive let preferReleaseBuild ← t.tryDecodeD `preferReleaseBuild false + let testRunner ← t.tryDecodeD `testRunner "" + let testDriver ← t.tryDecodeD `testDriver "" + let testDriver := if ¬testRunner.isEmpty ∧ testDriver.isEmpty then testRunner else testDriver + let testDriverArgs ← t.tryDecodeD `testDriverArgs #[] + let lintDriver ← t.tryDecodeD `lintDriver "" + let lintDriverArgs ← t.tryDecodeD `lintDriverArgs #[] let toLeanConfig ← tryDecode <| LeanConfig.decodeToml t let toWorkspaceConfig ← tryDecode <| WorkspaceConfig.decodeToml t return { name, precompileModules, moreGlobalServerArgs, srcDir, buildDir, leanLibDir, nativeLibDir, binDir, irDir, releaseRepo, buildArchive?, preferReleaseBuild + testDriver, testDriverArgs, lintDriver, lintDriverArgs toLeanConfig, toWorkspaceConfig } @@ -259,12 +266,11 @@ 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, testRunner + defaultTargets } if errs.isEmpty then return pkg diff --git a/src/lake/Lake/Toml/Encode.lean b/src/lake/Lake/Toml/Encode.lean index c304ec37ba..a3fde0ed4e 100644 --- a/src/lake/Lake/Toml/Encode.lean +++ b/src/lake/Lake/Toml/Encode.lean @@ -43,8 +43,6 @@ namespace Toml.Table @[inline] nonrec def insert [enc : ToToml α] (k : Name) (v : α) (t : Table) : Table := t.insert k (enc.toToml v) -instance (priority := low) [ToToml α] : SmartInsert α := ⟨Table.insert⟩ - /-- If the value is not `none`, inserts the encoded value into the table. -/ @[inline] nonrec def insertSome [enc : ToToml α] (k : Name) (v? : Option α) (t : Table) : Table := t.insertSome k (v?.map enc.toToml) @@ -61,6 +59,9 @@ instance : SmartInsert Table where instance [ToToml (Array α)] : SmartInsert (Array α) where smartInsert k v t := t.insertUnless v.isEmpty k (toToml v) +instance : SmartInsert String where + smartInsert k v t := t.insertUnless v.isEmpty k (toToml v) + /-- Insert a value into the table if `p` is `true`. -/ @[inline] nonrec def insertIf [enc : ToToml α] (p : Bool) (k : Name) (v : α) (t : Table) : Table := t.insertIf p k (enc.toToml v) diff --git a/src/lake/README.md b/src/lake/README.md index c052ec3187..e08bf9e64e 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -15,6 +15,7 @@ Each `lakefile.lean` includes a `package` declaration (akin to `main`) which def * [Package Configuration Options](#package-configuration-options) + [Layout](#layout) + [Build & Run](#build--run) + + [Test & Lint](#test--lint) + [Cloud Releases](#cloud-releases) * [Defining Build Targets](#defining-build-targets) + [Lean Libraries](#lean-libraries) @@ -164,8 +165,10 @@ Lake provides a large assortment of configuration options for packages. ### Layout +These options control the top-level directory layout of the package and its build directory. Further paths specified by libraries, executables, and targets within the package are relative to these directories. + * `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `.lake/packages`. -* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.) +* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`. * `leanLibDir`: The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., `.olean`, `.ilean` files). Defaults to `lib`. * `nativeLibDir`: The build subdirectory to which Lake should output the package's native libraries (e.g., `.a`, `.so`, `.dll` files). Defaults to `lib`. @@ -174,6 +177,8 @@ Lake provides a large assortment of configuration options for packages. ### Build & Run +These options configure how code is built and run in the package. Libraries, executables, and other targets within a package can further add to parts of this configuration. + * `platformIndependent`: Asserts whether Lake should assume Lean modules are platform-independent. That is, whether lake should include the platform and platform-dependent elements in a module's trace. See the docstring of `Lake.LeanConfig.platformIndependent` for more details. Defaults to `none`. * `precompileModules`: Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`. * `moreServerOptions`: An `Array` of additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. @@ -188,8 +193,21 @@ Lake provides a large assortment of configuration options for packages. * `weakLinkArgs`: An `Array` of additional arguments to pass to `leanc` when linking (e.g., binary executables or shared libraries) Unlike `moreLinkArgs`, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild. They come *before* `moreLinkArgs`. * `extraDepTargets`: An `Array` of [target](#custom-targets) names that the package should always build before anything else. +### Test & Lint + +The CLI commands `lake test` and `lake lint` use definitions configured by the workspace's root package to perform testing and linting (this referred to as the test or lint *driver*). In Lean configuration files, these can be specified by applying the `@[test_driver]` or `@[lint_driver]` to a `script`, `lean_exe`, or `lean_lb`. They can also be configured (in Lean or TOML format) via the following options on the package. + +* `testDriver`: The name of the script, executable, or library to drive `lake test`. +* `testDriverArgs`: An `Array` of arguments to pass to the package's test driver. +* `lintDriver`: The name of the script or executable used by `lake lint`. Libraries cannot be lint drivers. +* `lintDriverArgs`: An `Array` of arguments to pass to the package's lint driver. + +You can specify definition from a dependency as a package's test or lint driver by using the syntax `/`. An executable driver will be built and then run, a script driver will just be run, and a library driver will just be built. A script or executable driver is run with any arguments configured by package (e.g., via `testDriverArgs`) followed by any specified on the CLI (e.g., via `lake lint -- ...`). + ### Cloud Releases +These options define a cloud release for the package. See the section on [GitHub Release Builds](#github-release-builds) for more information. + * `releaseRepo`: The URL of the GitHub repository to upload and download releases of this package. If `none` (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default. * `buildArchive`: The name of the build archive for the GitHub cloud release. Defaults to `{(pkg-)name}-{System.Platform.target}.tar.gz`. diff --git a/src/lake/tests/driver/Test.lean b/src/lake/tests/driver/Test.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/lake/tests/test/clean.sh b/src/lake/tests/driver/clean.sh similarity index 100% rename from src/lake/tests/test/clean.sh rename to src/lake/tests/driver/clean.sh diff --git a/src/lake/tests/driver/dep-invalid.lean b/src/lake/tests/driver/dep-invalid.lean new file mode 100644 index 0000000000..99ab35ba6a --- /dev/null +++ b/src/lake/tests/driver/dep-invalid.lean @@ -0,0 +1,6 @@ +import Lake +open Lake DSL + +package test where + testDriver := "dep/driver/foo" + lintDriver := "dep/driver/foo" diff --git a/src/lake/tests/driver/dep-invalid.toml b/src/lake/tests/driver/dep-invalid.toml new file mode 100644 index 0000000000..f45df969bb --- /dev/null +++ b/src/lake/tests/driver/dep-invalid.toml @@ -0,0 +1,3 @@ +name = "test" +testDriver = "dep/driver/foo" +lintDriver = "dep/driver/foo" diff --git a/src/lake/tests/driver/dep-unknown.lean b/src/lake/tests/driver/dep-unknown.lean new file mode 100644 index 0000000000..b89f0cd7d7 --- /dev/null +++ b/src/lake/tests/driver/dep-unknown.lean @@ -0,0 +1,6 @@ +import Lake +open Lake DSL + +package test where + testDriver := "dep/driver" + lintDriver := "dep/driver" diff --git a/src/lake/tests/driver/dep-unknown.toml b/src/lake/tests/driver/dep-unknown.toml new file mode 100644 index 0000000000..d91ef99e62 --- /dev/null +++ b/src/lake/tests/driver/dep-unknown.toml @@ -0,0 +1,3 @@ +name = "test" +testDriver = "dep/driver" +lintDriver = "dep/driver" diff --git a/src/lake/tests/driver/dep.lean b/src/lake/tests/driver/dep.lean new file mode 100644 index 0000000000..67ec4f2d97 --- /dev/null +++ b/src/lake/tests/driver/dep.lean @@ -0,0 +1,8 @@ +import Lake +open Lake DSL + +package test where + testDriver := "dep/driver" + lintDriver := "dep/driver" + +require dep from "dep" diff --git a/src/lake/tests/driver/dep.toml b/src/lake/tests/driver/dep.toml new file mode 100644 index 0000000000..29642fdf6e --- /dev/null +++ b/src/lake/tests/driver/dep.toml @@ -0,0 +1,7 @@ +name = "test" +testDriver = "dep/driver" +lintDriver = "dep/driver" + +[[require]] +name = "dep" +path = "dep" diff --git a/src/lake/tests/driver/dep/lakefile.lean b/src/lake/tests/driver/dep/lakefile.lean new file mode 100644 index 0000000000..1442b8f7a0 --- /dev/null +++ b/src/lake/tests/driver/dep/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open System Lake DSL + +package dep + +@[test_driver, lint_driver] +script driver args do + IO.println s!"dep: {args}" + return 0 diff --git a/src/lake/tests/test/test.lean b/src/lake/tests/driver/driver.lean similarity index 100% rename from src/lake/tests/test/test.lean rename to src/lake/tests/driver/driver.lean diff --git a/src/lake/tests/driver/exe.lean b/src/lake/tests/driver/exe.lean new file mode 100644 index 0000000000..c54cec5278 --- /dev/null +++ b/src/lake/tests/driver/exe.lean @@ -0,0 +1,7 @@ +import Lake +open System Lake DSL + +package test + +@[test_driver, lint_driver] +lean_exe driver diff --git a/src/lake/tests/driver/exe.toml b/src/lake/tests/driver/exe.toml new file mode 100644 index 0000000000..9910fa2ec2 --- /dev/null +++ b/src/lake/tests/driver/exe.toml @@ -0,0 +1,6 @@ +name = "test" +testDriver = "driver" +lintDriver = "driver" + +[[lean_exe]] +name = "driver" diff --git a/src/lake/tests/driver/lib.lean b/src/lake/tests/driver/lib.lean new file mode 100644 index 0000000000..233754d489 --- /dev/null +++ b/src/lake/tests/driver/lib.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package test + +@[test_driver] +lean_lib Test diff --git a/src/lake/tests/driver/lib.toml b/src/lake/tests/driver/lib.toml new file mode 100644 index 0000000000..64669d2c12 --- /dev/null +++ b/src/lake/tests/driver/lib.toml @@ -0,0 +1,5 @@ +name = "test" +testDriver = "Test" + +[[lean_lib]] +name = "Test" diff --git a/src/lake/tests/test/none.lean b/src/lake/tests/driver/none.lean similarity index 100% rename from src/lake/tests/test/none.lean rename to src/lake/tests/driver/none.lean diff --git a/src/lake/tests/test/none.toml b/src/lake/tests/driver/none.toml similarity index 100% rename from src/lake/tests/test/none.toml rename to src/lake/tests/driver/none.toml diff --git a/src/lake/tests/test/exe.lean b/src/lake/tests/driver/runner.lean similarity index 79% rename from src/lake/tests/test/exe.lean rename to src/lake/tests/driver/runner.lean index 59a2f3fbcd..eae831b568 100644 --- a/src/lake/tests/test/exe.lean +++ b/src/lake/tests/driver/runner.lean @@ -4,4 +4,4 @@ open System Lake DSL package test @[test_runner] -lean_exe test +lean_exe driver diff --git a/src/lake/tests/driver/runner.toml b/src/lake/tests/driver/runner.toml new file mode 100644 index 0000000000..1a83357868 --- /dev/null +++ b/src/lake/tests/driver/runner.toml @@ -0,0 +1,5 @@ +name = "test" +testRunner = "driver" + +[[lean_exe]] +name = "driver" diff --git a/src/lake/tests/test/script.lean b/src/lake/tests/driver/script.lean similarity index 64% rename from src/lake/tests/test/script.lean rename to src/lake/tests/driver/script.lean index d6ce2585f0..8658b60400 100644 --- a/src/lake/tests/test/script.lean +++ b/src/lake/tests/driver/script.lean @@ -3,7 +3,7 @@ open System Lake DSL package test -@[test_runner] -script test args do +@[test_driver, lint_driver] +script driver args do IO.println s!"script: {args}" return 0 diff --git a/src/lake/tests/driver/test.sh b/src/lake/tests/driver/test.sh new file mode 100755 index 0000000000..29f1538f10 --- /dev/null +++ b/src/lake/tests/driver/test.sh @@ -0,0 +1,86 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LAKE=${LAKE:-../../.lake/build/bin/lake} + +./clean.sh + +# Script driver +$LAKE -f script.lean test | grep --color -F "script: []" +$LAKE -f script.lean lint | grep --color -F "script: []" +$LAKE -f script.lean test -- hello | grep --color "hello" +$LAKE -f script.lean lint -- hello | grep --color "hello" + +# Executable driver +$LAKE -f exe.lean test | grep --color -F "exe: []" +$LAKE -f exe.toml test | grep --color -F "exe: []" +$LAKE -f exe.lean lint | grep --color -F "exe: []" +$LAKE -f exe.toml lint | grep --color -F "exe: []" +$LAKE -f exe.lean test -- hello | grep --color "hello" +$LAKE -f exe.toml test -- hello | grep --color "hello" +$LAKE -f exe.lean lint -- hello | grep --color "hello" +$LAKE -f exe.toml lint -- hello | grep --color "hello" + +# Library test driver +rm -f .lake/build/lib/Test.olean +$LAKE -f lib.lean test | grep --color -F "Built Test" +rm -f .lake/build/lib/Test.olean +$LAKE -f lib.toml test | grep --color -F "Built Test" +($LAKE -f lib.lean test -- hello 2>&1 && exit 1 || true) | grep --color "arguments cannot be passed" +($LAKE -f lib.toml test -- hello 2>&1 && exit 1 || true) | grep --color "arguments cannot be passed" + +# Upstream driver +rm -f lake-manifest.json +$LAKE -f dep.lean test | grep --color -F "dep: []" +$LAKE -f dep.toml test | grep --color -F "dep: []" +$LAKE -f dep.lean lint | grep --color -F "dep: []" +$LAKE -f dep.toml lint | grep --color -F "dep: []" +$LAKE -f dep.lean test -- hello | grep --color "hello" +$LAKE -f dep.toml test -- hello | grep --color "hello" +$LAKE -f dep.lean lint -- hello | grep --color "hello" +$LAKE -f dep.toml lint -- hello | grep --color "hello" + +# Test runner +$LAKE -f runner.lean test 2>&1 | grep --color -F " @[test_runner] has been deprecated" +$LAKE -f runner.toml test +$LAKE -f runner.lean check-test +$LAKE -f runner.toml check-test + +# Driver validation +($LAKE -f two.lean test 2>&1 && exit 1 || true) | grep --color "only one" +($LAKE -f none.lean test 2>&1 && exit 1 || true) | grep --color "no test driver" +($LAKE -f none.toml test 2>&1 && exit 1 || true) | grep --color "no test driver" +($LAKE -f unknown.lean test 2>&1 && exit 1 || true) | grep --color "invalid test driver: unknown" +($LAKE -f unknown.toml test 2>&1 && exit 1 || true) | grep --color "invalid test driver: unknown" +($LAKE -f dep-unknown.lean test 2>&1 && exit 1 || true) | grep --color "unknown test driver package" +($LAKE -f dep-unknown.toml test 2>&1 && exit 1 || true) | grep --color "unknown test driver package" +($LAKE -f dep-invalid.lean test 2>&1 && exit 1 || true) | grep --color "invalid test driver" +($LAKE -f dep-invalid.toml test 2>&1 && exit 1 || true) | grep --color "invalid test driver" +($LAKE -f two.lean lint 2>&1 && exit 1 || true) | grep --color "only one" +($LAKE -f none.lean lint 2>&1 && exit 1 || true) | grep --color "no lint driver" +($LAKE -f none.toml lint 2>&1 && exit 1 || true) | grep --color "no lint driver" +($LAKE -f unknown.lean lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver: unknown" +($LAKE -f unknown.toml lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver: unknown" +($LAKE -f dep-unknown.lean lint 2>&1 && exit 1 || true) | grep --color "unknown lint driver package" +($LAKE -f dep-unknown.toml lint 2>&1 && exit 1 || true) | grep --color "unknown lint driver package" +($LAKE -f dep-invalid.lean lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver" +($LAKE -f dep-invalid.toml lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver" + +# Driver checker +$LAKE -f exe.lean check-test +$LAKE -f exe.toml check-test +$LAKE -f exe.lean check-lint +$LAKE -f exe.toml check-lint +$LAKE -f dep.lean check-test +$LAKE -f dep.toml check-test +$LAKE -f dep.lean check-lint +$LAKE -f dep.toml check-lint +$LAKE -f script.lean check-test +$LAKE -f script.lean check-lint +$LAKE -f lib.lean check-test +$LAKE -f two.lean check-test && exit 1 || true +$LAKE -f two.lean check-lint && exit 1 || true +$LAKE -f none.lean check-test && exit 1 || true +$LAKE -f none.toml check-test && exit 1 || true +$LAKE -f none.lean check-lint && exit 1 || true +$LAKE -f none.toml check-lint && exit 1 || true diff --git a/src/lake/tests/test/two.lean b/src/lake/tests/driver/two.lean similarity index 63% rename from src/lake/tests/test/two.lean rename to src/lake/tests/driver/two.lean index 28cd7dd01b..2ff68472da 100644 --- a/src/lake/tests/test/two.lean +++ b/src/lake/tests/driver/two.lean @@ -3,8 +3,8 @@ open System Lake DSL package test -@[test_runner] +@[test_driver, lint_driver] lean_exe testExe -@[test_runner] +@[test_driver, lint_driver] script testScript do return 1 diff --git a/src/lake/tests/driver/unknown.lean b/src/lake/tests/driver/unknown.lean new file mode 100644 index 0000000000..614497447b --- /dev/null +++ b/src/lake/tests/driver/unknown.lean @@ -0,0 +1,6 @@ +import Lake +open System Lake DSL + +package test where + testDriver := "invalid" + lintDriver := "invalid" diff --git a/src/lake/tests/driver/unknown.toml b/src/lake/tests/driver/unknown.toml new file mode 100644 index 0000000000..3240df6c83 --- /dev/null +++ b/src/lake/tests/driver/unknown.toml @@ -0,0 +1,3 @@ +name = "test" +testDriver = "invalid" +lintDriver = "invalid" diff --git a/src/lake/tests/test/exe.toml b/src/lake/tests/test/exe.toml deleted file mode 100644 index e1f3289bdc..0000000000 --- a/src/lake/tests/test/exe.toml +++ /dev/null @@ -1,5 +0,0 @@ -name = "test" -testRunner = "test" - -[[lean_exe]] -name = "test" diff --git a/src/lake/tests/test/test.sh b/src/lake/tests/test/test.sh deleted file mode 100755 index 7892b16141..0000000000 --- a/src/lake/tests/test/test.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/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 && exit 1 || true) | grep --color "only one" -($LAKE -f none.lean test 2>&1 && exit 1 || true) | grep --color "no test runner" -($LAKE -f none.toml test 2>&1 && exit 1 || 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 && exit 1 || true) -($LAKE -f none.lean check-test && exit 1 || true) -($LAKE -f none.toml check-test && exit 1 || true) diff --git a/src/lake/tests/translateConfig/out.expected.lean b/src/lake/tests/translateConfig/out.expected.lean index 86d105d738..d009747a4a 100644 --- a/src/lake/tests/translateConfig/out.expected.lean +++ b/src/lake/tests/translateConfig/out.expected.lean @@ -5,6 +5,8 @@ open System Lake DSL package test where releaseRepo := "" buildArchive := "" + testDriver := "b" + lintDriver := "b" platformIndependent := true require foo from "-" with Lake.NameMap.empty |>.insert `foo "bar" @@ -13,4 +15,4 @@ require bar from git "https://example.com"@"abc"/"sub/dir" @[default_target] lean_lib A -@[test_runner] lean_exe b +lean_exe b diff --git a/src/lake/tests/translateConfig/out.expected.toml b/src/lake/tests/translateConfig/out.expected.toml index 6530167e9b..27414cdc3f 100644 --- a/src/lake/tests/translateConfig/out.expected.toml +++ b/src/lake/tests/translateConfig/out.expected.toml @@ -1,5 +1,6 @@ name = "test" -testRunner = "b" +testDriver = "b" +lintDriver = "b" defaultTargets = ["A"] [leanOptions] diff --git a/src/lake/tests/translateConfig/source.lean b/src/lake/tests/translateConfig/source.lean index 00fd81f309..0bae023822 100644 --- a/src/lake/tests/translateConfig/source.lean +++ b/src/lake/tests/translateConfig/source.lean @@ -30,6 +30,7 @@ package test where preferReleaseBuild := false packagesDir := defaultPackagesDir leanOptions := #[⟨`pp.unicode.fun, true⟩] + lintDriver := "b" require foo from "dir" with NameMap.empty.insert `foo "bar" require bar from git "https://example.com" @ "abc" / "sub" / "dir" @@ -45,7 +46,7 @@ lean_lib A where nativeFacets := fun _ => #[] toLeanConfig := testLeanConfig -@[test_runner] +@[test_driver] lean_exe b where srcDir := "." root := `b diff --git a/src/lake/tests/translateConfig/source.toml b/src/lake/tests/translateConfig/source.toml index d190465c35..161ace2819 100644 --- a/src/lake/tests/translateConfig/source.toml +++ b/src/lake/tests/translateConfig/source.toml @@ -1,4 +1,5 @@ -testRunner = "b" +testDriver = "b" +lintDriver = "b" defaultTargets = ['A'] name = "test"