Commit 2024-05-20 07:13 7a03bae6
View on Github →chore: switch from make test to lake test (#12943)
In an effort to start moving to a more Lean+Lake based infrastructure, this installs a test runner which is a thin wrapper around Batteries' test runner introduced in https://github.com/leanprover-community/batteries/pull/787.
The liskin/gh-problem-matcher-wrap@v3 problem matcher was already broken for the test suite, and will remain broken here. There's a tracking issue at #12946. We can restore that once the new test behaviour has converged.