From 4a801a673c33e2091ee72d4a1f55df89c1b8860e Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 23 May 2024 21:37:34 -0400
Subject: [PATCH] chore: fix translateConfig test + related touchups

---
 src/lake/Lake/CLI/Help.lean                      |  6 ++++++
 src/lake/Lake/CLI/Main.lean                      | 11 +++++------
 src/lake/Lake/CLI/Translate/Lean.lean            | 12 +++++++-----
 src/lake/Lake/Load/Main.lean                     | 11 ++++++++---
 src/lake/tests/translateConfig/out.expected.lean |  4 +++-
 src/lake/tests/translateConfig/out.expected.toml |  3 ++-
 src/lake/tests/translateConfig/source.lean       |  3 ++-
 src/lake/tests/translateConfig/source.toml       |  3 ++-
 8 files changed, 35 insertions(+), 18 deletions(-)

diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 70cfa299d68d..f75f23e9dec5 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -168,6 +168,9 @@ USAGE:
 
 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 :=
@@ -194,6 +197,9 @@ USAGE:
 
 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 :=
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 9dcf5aceaf9f..3b4eaaf5ed15 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -353,8 +353,8 @@ protected def test : CliM PUnit := do
 
 protected def checkTest : CliM PUnit := do
   processOptions lakeOption
-  let ws ← loadWorkspace ( ← mkLoadConfig (← getThe LakeOptions))
-  noArgsRem do exit <| if ws.root.testDriver.isEmpty 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
@@ -366,8 +366,8 @@ protected def lint : CliM PUnit := do
 
 protected def checkLint : CliM PUnit := do
   processOptions lakeOption
-  let ws ← loadWorkspace ( ← mkLoadConfig (← getThe LakeOptions))
-  noArgsRem do exit <| if ws.root.lintDriver.isEmpty then 1 else 0
+  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
@@ -452,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)
diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 4da2b8c3d04f..6d71f5ab5209 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,9 +104,9 @@ 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 cfg.testDriver ""
+    |> addDeclFieldD `testDriver testDriver ""
     |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
-    |> addDeclFieldD `lintDriver cfg.lintDriver ""
+    |> addDeclFieldD `lintDriver lintDriver ""
     |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
     |> cfg.toWorkspaceConfig.addDeclFields
     |> cfg.toLeanConfig.addDeclFields
@@ -176,7 +178,7 @@ 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 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)
diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index b1defb98a64f..df7d703d612d 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/tests/translateConfig/out.expected.lean b/src/lake/tests/translateConfig/out.expected.lean
index 86d105d7388f..d009747a4a8e 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 6530167e9b1b..27414cdc3f4c 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 00fd81f309fc..0bae0238220f 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 d190465c350c..161ace28195a 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"