how to test lean code

Stream: lean4

[Christian Pehle]

Are there any plans in the community to write a test framework? The solutions I'm aware of so far are the one used by lean itself, which I have been able to partially replicate following the example of (https://github.com/tydeu/lean4-papyrus) for a package that I'm developing and I've also seen extended assertion support somewhere. What are your thoughts?

[Henrik Böving]

Yes there are! This is a first draft for a quickcheck clone https://github.com/leanprover-community/mathlib4/pull/254 that might be merged into mathlib (and later pulled out into a seperate package) today

[Henrik Böving]

Eventually I'm hoping to write something additional that sort of resembles spec tests and can be converted to normal proofs easily. That is, if you decide to verify your properties the effort should be the verification and not fiddling with the test framework.

[Arthur Paulino]

It got me thinking about using metaprogramming in order to check for test coverage. Might be a fun exercise