From a1578ecc8f1ed2f7bef68f3ff7c321bfc0c49820 Mon Sep 17 00:00:00 2001
From: Matthew Robert Ballard <matt@mrb.email>
Date: Fri, 25 Oct 2024 00:50:18 +0000
Subject: [PATCH] chore: use `Batteries` test driver directly in the lake file
 (#15897)

With leanprover/lean4#4261, we can specify a test driver from a dependency. We do this with `Batteries` test driver. Previously, the test driver from `Batteries` was called via `scripts/test.lean` which is now removed.
---
 lakefile.lean     | 14 ++------------
 scripts/test.lean | 21 ---------------------
 2 files changed, 2 insertions(+), 33 deletions(-)
 delete mode 100644 scripts/test.lean

diff --git a/lakefile.lean b/lakefile.lean
index 697f41bab4e5b..25b17ebe85a33 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -52,6 +52,8 @@ package mathlib where
   leanOptions := mathlibLeanOptions
   -- Mathlib also enforces these linter options, which are not active by default.
   moreServerOptions := mathlibOnlyLinters
+  -- Use Batteries' test driver for `lake test`
+  testDriver := "batteries/test"
   -- These are additional settings which do not affect the lake hash,
   -- so they can be enabled in CI and disabled locally or vice versa.
   -- Warning: Do not put any options here that actually change the olean files,
@@ -132,18 +134,6 @@ lean_exe pole where
   -- Executables which import `Lake` must set `-lLake`.
   weakLinkArgs := #["-lLake"]
 
-/--
-`lake exe test` is a thin wrapper around `lake exe batteries/test`, until
-https://github.com/leanprover/lean4/issues/4121 is resolved.
-
-You can also use it as e.g. `lake exe test conv eval_elab` to only run the named tests.
--/
-@[test_driver]
-lean_exe test where
-  -- We could add the above `leanOptions` and `moreServerOptions`: currently, these do not take
-  -- effect as `test` is a `lean_exe`. With a `lean_lib`, it would work...
-  srcDir := "scripts"
-
 /-!
 ## Other configuration
 -/
diff --git a/scripts/test.lean b/scripts/test.lean
deleted file mode 100644
index f02a621637377..0000000000000
--- a/scripts/test.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-/-
-Copyright (c) 2024 Kim Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-open IO.Process
-open System
-
-/--
-Run tests, via the Batteries test runner.
-
-When https://github.com/leanprover/lean4/issues/4121
-"allow using an upstream executable as a lake `@[test_runner]`"
-is resolved, this file can be replaced with a line in `lakefile.lean`.
--/
-def main (args : List String) : IO Unit := do
-  -- ProofWidgets and Batteries may not have been completely built by `lake build` yet,
-  -- but they are needed by some tests.
-  _ ← (← spawn { cmd := "lake", args := #["build", "ProofWidgets", "Batteries"] }).wait
-  let exitcode ← (← spawn { cmd := "lake", args := #["exe", "batteries/test"] ++ args }).wait
-  exit exitcode.toUInt8