How to write (idiomatic) tests in Lean 4?

Stream: lean4

[Santtu]

What the title says. I've been trying to find information about what the idiomatic way of writing tests in Lean 4 is supposed to be, but that information seems to be under some rock. Also, how do I run the tests once I have written them? I see lake has a command test, but the help for lake test talks about some "test driver", and I've still to find a clearly written example of this. Do I need to set it up in lakefile.toml?

[Siddhartha Gadgil]

Yes, you need a lakefile.toml or a lakefile.lean, but you need this for any lean project. Here is an example lakefile.toml with a test driver.

name = "LeanSearchClient"
testDriver = "LeanSearchClientTest"
defaultTargets = ["LeanSearchClient"]

[[lean_lib]]
name = "LeanSearchClient"

[[lean_lib]]
name = "LeanSearchClientTest"

The library LeanSearchClientTest has the test files, which are simply Lean files. A useful way to write tests is to use guard_msgs before a command say #eval ... or #check ....

/-- info: 2 -/
#guard_msgs in
#eval 1 + 1

The great thing about #guard_msgs is if you just include it, you will get a code action to add the correct stuff.

[Santtu]

Right, having the tests as a separate library makes sense. And I suppose that marking the tests library as a test driver makes it possible to import stuff from the actual library?

[Eric Wieser]

I think the lean_lib is what makes the imports resolve; the testDriver just hooks it up to lake test

[Tomas Skrivan]

What is the idiomatic way to run compiled tests?

I.e. I have a bunch of lean files with def main : IO Int := ... which should return 0 when executed.

I do now want to list all those files in lakefile but say that all files in a directory should be treated that way.