[Merged by Bors] - chore: use Batteries test driver directly in the lake file

lakefile.lean

@@ -29,6 +29,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,
@@ -111,18 +113,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
 -/