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.

[Arthur Paulino]

Hello, I'd like to (re)use this thread to ask about the following goal for the year 3 roadmap:

5. Provide reliable benchmarking, testing, and profiling infrastructure for Lean and Mathlib.

More specifically, I'm interested in the testing infrastructure.

As a reference, we've been using LSpec to test Lean 4 code. It has decent ways to define testing suites. It also has API for property testing, which is extremely useful.

However, one major issue of LSpec is that it currently runs the tests simply by importing test suites. I think this happens because LSpec is based on Prop decidability to derive Testable

/--
The main typeclass of propositions that can be tested by `LSpec`.

In non-succeeding cases, it may contain an explanatory message.
-/
class inductive Testable (p : Prop) where
  | isTrue  (h : p)
  | isMaybe (msg : Option String := none)
  | isFalse (h : ¬ p) (msg : Option String := none)
  | isFailure (msg : Option String := none)

/-- A default `Testable` instance with low priority. -/
instance (priority := 25) (p : Prop) [d : Decidable p] : Testable p :=
  match d with
  | isFalse h => .isFalse h "Evaluated to false"
  | isTrue  h => .isTrue  h

All that to motivate the questions: what are the plans for the official Lean 4 testing infrastructure? Will it support property testing natively?

[Henrik Böving]

The benchmarking and profiling part of this is more geared towards work on velcom (known to most as https://speed.lean-lang.org/) done by Joscha Mennicken.

The plans for the testing infrastructure are much less laid out at the moment. There was a time where I worked on a generic testing infrastructure that can handle many kinds of tests here https://github.com/hargoniX/nest-core (and in related nest- repositories) though I eventually stopped. I guess if we revitalized that kind of infrastructure we could have spec tests, property tests, golden tests and all the other stuff that people are interested in.

[Arthur Paulino]

Okay I already see that IsTest.run happens in IO and therefore it wouldn't have this issue of running tests just by importing them.

I'm looking forward to it!

[Alfredo Moreira-Rosa]

Nice, nest-unit looks really neat. I Hope something like this makes it into Std.