test runner

Stream: mathlib4

[Quinn]

I don't see the test runner in lakefile https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean where in lean4 projects do you configure the test runner? what's the command to run the tests?

[Kim Morrison]

Right now there is no test runner, and every project does something different (usually make test).

As of v4.8.0-rc1, out in a day or two hopefully, there will be lake test. Initially, that will just be a hook behind which you still need to roll your own test runner, but the idea is to standardise on lake test as the command, and gradually add more features in Lake itself.

[Quinn]

cool!

[Kim Morrison]

lake test arrived in https://github.com/leanprover/lean4/pull/3779