Zulip Chat Archive

Stream: lean4

Topic: simple interactive unit testing?


Andrew Kent (Feb 05 2021 at 18:57):

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 (Feb 05 2021 at 19:51):

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

Andrew Kent (Feb 05 2021 at 20:18):

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

Sebastian Ullrich (Feb 05 2021 at 22:13):

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

Andrew Kent (Feb 07 2021 at 02:25):

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 (Feb 07 2021 at 02:26):

ex_assert_via.png ex_assert.png ex_failed_assert.png

Max Nowak (May 26 2022 at 10:37):

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 (May 27 2022 at 05:09):

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 (May 27 2022 at 05:10):

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 (May 27 2022 at 05:26):

(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?)


Last updated: Dec 20 2023 at 11:08 UTC