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

[mattrobball]

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.

---

[github-actions]

PR summary b4abd0ebc7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- main

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mattrobball]

@kim-em I was looking at lake test for my class and noticed this todo. Local testing seems good but you would know better. Let me know if anything is amiss.

[adomani]

I don't really know how to review this, since I do not know the implications of the changes! However, I can see that CI was successful and that the tests have been run, so this looks good to me! 😄

[bryangingechen]

@semorrison Could you take a look at this when you have a spare moment?

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style