Zulip Chat Archive

Stream: lean4

Topic: simple interactive unit testing?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Sebastian Ullrich (Feb 05 2021 at 22:13):

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

view this post on Zulip 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

view this post on Zulip Andrew Kent (Feb 07 2021 at 02:26):

ex_assert_via.png ex_assert.png ex_failed_assert.png


Last updated: May 07 2021 at 12:15 UTC