simple interactive unit testing?

Stream: lean4

[Andrew Kent]

I'm curious, has anyone come up with a simple, cute unit testing technique?

I've done a little tinkering, and using something like this checkBEq function

-- Test.lean
open Lean Std

def checkBEq {α} [BEq α] [Repr α] (actual expected : α) : IO Unit :=
  if actual == expected
  then IO.println "pass"
  else do
    let actualStr := toString (Format.indentD (Format.append (Format.text "  actual ") (Repr.addAppParen (reprArg actual) 0)))
    let expectedStr := toString (Format.indentD (Format.append (Format.text "expected ") (Repr.addAppParen (reprArg expected) 0)))
    throw $ IO.userError s!"fail{actualStr}{expectedStr}"

with #eval isn't the worst. E.g.,

#eval checkBEq 1 1
#eval checkBEq 1 2

will print the following when the file is run:

pass

Test.lean:12:0: error: fail
    actual 1
  expected 2

which is most of what I want. In particular, I'm going for

1. it to be trivial to calculate pass/fail counts by examining the output, and
2. failures that give enough information for quick debugging (i.e., line number and expected vs actual value comparison)

The one thing I'm really wishing it did though was trigger the interactive "red error squiggles" in IDEs using Lean4's language server. There's not a simple way to add such interactive feedback anyone can think of... is there?

[Mario Carneiro]

You can probably get the squiggles by using a macro for checkBEq and running the test in the macro's elaboration

[Andrew Kent]

Interesting idea... perhaps the #eval macro commands's impl has just the sort of macrology I need...

[Sebastian Ullrich]

For inspiration see e.g. https://docs.rs/assert2/0.3.4/assert2/

[Andrew Kent]

It could use some improvements and additional features, but here's a first draft I'm pretty happy with =)
https://github.com/pnwamk/lean4-assert-command

[Andrew Kent]

ex_assert_via.png ex_assert.png ex_failed_assert.png

[Max Nowak]

This is great! Though, it is not quite there yet with what unit tests provide. I envision a future where all it takes to write a test is some annotation on a function, and then running lake test will just work. Has anyone been working on something like that? I don't know what people prefer, but I really like the Rust approach of writing tests in the same file, since that has a very low mental threshold to do (no need to set up a tests directory, etc).

[James Gallicchio]

I'm kind of more a fan of having tests not in the same directory, at least for anything beyond simple sanity checks... It can junk up source files, and can make it more awkward to build generic tests (e.g. you have some tests you want to run on two implementations of the same interface; what file do you put them in?).

What about doc-esque links from source code to tests? That way you could keep tests somewhere separate but still easily navigate to relevant tests when you want to. Never heard of that kind of approach but I feel like I'd like it?

[James Gallicchio]

It would be super cool if you could link from a comment explaining some patch in your code to a test that makes sure the patch is doing what it's supposed to do :D

[James Gallicchio]

(Although, these can definitely co-exist in Lean; interactive unit tests in the relevant source files for basic sanity checks, + more heavyweight unit testing with tests located outside the main project?)