How to create and run unit tests?

Stream: new members

[Krishna Padmasola]

Hello Friends,
Is there a way I can create a test suite containing unit tests and run them to get a report?
I could not find any tutorial documentation for this.
I am looking at using Lean as a programming language rather than as a theorem prover, at least initially, since I am more familiar with programming (in other languages, such as Java) than with theorem proving.
Any links to existing testsuites and instructions on how to run them would be very helpful.
thanks!

[Eric Wieser]

Today I don't think there is any standard way to do this. Mathlib's tests mostly make do with #guard_msg in #eval foo to test foo.

[Eric Wieser]

It's quite likely that there are people on this Zulip with prototype frameworks of their own

[Krishna Padmasola]

I found the lake test command and was able to get tests executed by adding them to a @[test_driver] section in lakefile.lean. But these tests are methods that print pass/fail messages after checking the appropriate result.
How does one run the #guard_msg in #eval foo type of tests? Do these tests also print a pass/fail report when executed?

[Eric Wieser]

The #guard_msg tests are ones that fail to compile if the comment doesn't match the actual output

[Eric Wieser]

There's no report beyond the standard display of lake compilation errors