Introducing the nest

Stream: lean4

[Henrik Böving]

I started implementing a lean variant of the haskell testing library/eco-system tasty (https://hackage.haskell.org/package/tasty-1.4.3).

It is a library that provides an extensible way to both declare and execute tests. The implementation of the core data structures lives here: https://github.com/hargoniX/nest-core and I wrote a basic assert based test provider here: https://github.com/hargoniX/nest-unit. Taking an example from the README you write your tests like so:

import NestCore
import NestUnit

open Nest.Core
open Nest.Unit

def fileRes (path : System.FilePath) (mode : IO.FS.Mode) : ResourceSpec IO.FS.Handle where
  get := IO.FS.Handle.mk path mode
  release handle := handle.flush
  description := s!"A file handle to {path}"

def tests : TestTree := [nest|
  group "Self Tests"
    group "Basic"
      test "succeeds on true" : UnitTest := do
        assert true
      test "fails on false (expected to fail)" : UnitTest := do
        assert false
    group "Resource based"
      with resource fileRes "/dev/zero" .read as res
        test "assertion 3" : UnitTest := do
          let data ← res.read 12
          assert data.size = 12
    group "Option based"
      with options fun x => x.insert `Hello "foo"
        with options as x
          test "assertion 4" : UnitTest := do
            assert x.contains `Hello
]

def main : IO UInt32 := Nest.Core.defaultMain tests

(If you are scared of the lots of custom syntax, it is just a very thin layer on top of TestTree which you can easily write out without the syntax as well, it is just a little cleaner this way).

The output of the above test would look as follows:

Running group Self Tests:
  Running group Basic:
    succeeds on true: all assertions succeeded [OK]
    fails on false (expected to fail): assertion failure: boolean was false [FAIL]
      file: './././Main.lean', line: 18, col: 8
  Running group Resource based:
    Acquiring resource: A file handle to /dev/zero
      assertion 3: all assertions succeeded [OK]
    Releasing resource
  Running group Option based:
    assertion 4: all assertions succeeded [OK]

Any feedback or feature wishes welcome^^

I was thinking about adding additional test providers for:

• golden tests, i.e. ones that compare to files
• property tests based on SlimCheck
• performance tests

[Joachim Breitner]

Pretty neat! It’s great to have all these tools around.

How bad would that example look like without custom syntax? I know custom syntax is fun to come up with and can often make a big difference, but it does add to the mental complexity of using a new tools, and maybe normal syntax (with good combinators) is good enough?

[Henrik Böving]

If you want to write it a singular decl like above it gets eh..rough:

def tests2 : TestTree :=
  .group "Self Tests" [
    .group "Basics" [
      .single "succeeds on true" (assert true),
      .single "fails on false" (assert false)
    ],
    .group "Resource based" [
      .withResource (fileRes "/dev/zero" .read) (fun res =>
        .single "assertion 3" (do
          let data ← res.read 12
          assert data.size = 12 : UnitTest)
      )
    ]
  ]

Although a lot of this can of course be mitigated by splitting it up into more declarations as i've seen tasty seems to do regularly?

def basics : TestTree :=
  .group "Basics" [
    .single "succeeds on true" (assert true),
    .single "fails on false" (assert false)
  ]

def resTest (res : IO.FS.Handle) : TestTree :=
 .single "assertion 3" (do
   let data ← res.read 12
   assert data.size = 12 : UnitTest) -- This is particularly annoying but I feel it can be fixed

def resBased : TestTree :=
  .group "Resource based" [
    .withResource (fileRes "/dev/zero" .read) resTest
  ]

def tests2 : TestTree :=
  .group "Self Tests" [
    basics,
    resBased
  ]

def main : IO UInt32 := Nest.Core.defaultMain tests2

[Henrik Böving]

@Joachim Breitner

[Joachim Breitner]

I find the first of these not particularly rough, and especially when reading it I'll have a much easier time understanding what's going on (in particular that there isn't much going on; these are just constructors), and not significantly less pretty than the custom syntax. And I'll make it easier for me to define my little helper functions if I don't have syntax to see through. But I am of course very much biased by having worked with tasty a lot :-)

[Joachim Breitner]

(Also sorry for following Wadler's law - you post a cool tool and the first feedback you get is on syntax :-))

[Joachim Breitner]

You don't need the parents around do and fun, do you? Without them it's even closer to the custom syntax. Ah, but there is a type annotation. I see.

[Henrik Böving]

Joachim Breitner said:

You don't need the parents around do and fun, do you? Without them it's even closer to the custom syntax. Ah, but there is a type annotation. I see.

The parens around the do in assertion 3 are necessary for the type annotation so that type inference works out properly (this is one of the reasons I added the custom syntax). I don't understand how you think it is possible to get rid of the fun in the first example though?

[Henrik Böving]

Oh or do you mean getting rid of the parens around fun?

[Joachim Breitner]

Yes, just a minor thing, but it increases prettiness if you don't have these closing parentheses flyting around code that's properly indented anyways (in my humble opinion)

[Henrik Böving]

Oh I also found a way to get rid off the annotation on do!

[Henrik Böving]

Let me update the readme

[Henrik Böving]

def tests : TestTree :=
  .group "Self Tests" [
    .group "Basics" [
      .single "succeeds on true" (assert true),
      .single "fails on false" (assert false)
    ],
    .group "Resource based" [
      .withResource (fileRes "/dev/zero" .read) fun res =>
        .single (t := UnitTest) "assertion 3" do
          let data ← res.read 12
          assert data.size = 12
    ],
    .group "Option based" [
      .withOptions (fun x => x.insert `Hello "foo") <|
        .getOptions fun x =>
          .single "assertion 4" (assert x.contains `Hello)
    ]
  ]

@Joachim Breitner \o/

[Joachim Breitner]

Just looking at this example, it seems assert isn't a plain function, is it?

[Henrik Böving]

Yes this is explained in nest-unit. I need it to be not a plain function for two reasons:
a) I want to print the location where it failed and I need a meta program snippet to figure out the location
b) I want to be able to also assert decidable propositions but if you look in the implementation of NestUnit you will see this requires a little trick to make compatible with the typeclass mechanism.

[Henrik Böving]

We dont have the HasCallStack thing that haskell has so a) is necessary. I tried to work around b) by using a coercion but that didn't kick in properly. You can write something explicit like assert <| Proxy.mk <| x = y but that seemed too much of a hassle

[Kyle Miller]

What's the purpose of Proxy? Is it to turn a value into a type so you can add Prop instances piecemeal?

It seems to me you could change Assertable to

class Assertable {α : Sort u} (x : α) where
  assertThis : UnitM Unit

and then for example you could write

instance [forall (x : t), Assertable x] (xs : List t) : Assertable xs where
  assertThis := xs.forM assertThis

and

instance [DecidableEq α] [Repr α] {x y : α} : Assertable (x = y) where
  assertThis := do
    unless x = y do
      assertFailure s!"equality failed, left: '{repr x}', right: '{repr y}'"

With this design, you don't need to conditionally insert Proxy.

[Henrik Böving]

Oh! That's awesome yes, I'll refactor to this approach

[Sebastian Ullrich]

HasCallStack could be simulated with auto params

[Henrik Böving]

Sebastian Ullrich said:

HasCallStack could be simulated with auto params

You mean that I inject the position via some custom elaborated pos% that gets auto paramed to the assert function?

[Henrik Böving]

Kyle Miller said:

What's the purpose of Proxy? Is it to turn a value into a type so you can add Prop instances piecemeal?

It seems to me you could change Assertable to

class Assertable {α : Sort u} (x : α) where
  assertThis : UnitM Unit

and then for example you could write

instance [forall (x : t), Assertable x] (xs : List t) : Assertable xs where
  assertThis := xs.forM assertThis

and

instance [DecidableEq α] [Repr α] {x y : α} : Assertable (x = y) where
  assertThis := do
    unless x = y do
      assertFailure s!"equality failed, left: '{repr x}', right: '{repr y}'"

With this design, you don't need to conditionally insert Proxy.

interestingly just

instance [forall (x : t), Assertable x] (xs : List t) : Assertable xs where
  assertThis := xs.forM assertThis

doesn't type check bu

instance [forall (x : t), Assertable x] (xs : List t) : Assertable xs where
  assertThis := xs.forM (assertThis ·)

does?

[Henrik Böving]

@Sebastian Ullrich I tried this now:

open Lean in
scoped elab "pos%" : term => do
  let some pos := (← getRef).getPos?
    | throwError "no source info"
  let pos := (← getFileMap).toPosition pos
  let posExpr := toExpr (← getFileName, pos)
  return posExpr

def assert (t : α) [Assertable t] (pos := pos%) : UnitM Unit :=
  try
    assertThis t
  catch e =>
    throw <| { e with pos := some pos }

but this gives me the wrong position (namely the location of the def assert) did you have something else in mind?

[Kyle Miller]

I think it might be (pos := by exact pos%) to defer it

[Kyle Miller]

Henrik Böving said:

interestingly just [...] doesn't type check but [...] does?

I'd guess it's because the new assertThis now has the instance argument coming after the x argument. Writing (assertThis ·) applies the function so it unlocks filling in the instance argument.

[Henrik Böving]

Kyle Miller said:

I think it might be (pos := by exact pos%) to defer it

indeed, makes sense.

[Henrik Böving]

https://github.com/hargoniX/nest-unit pushed, now with 90% less meta magic and 90% more type theory magic :P

[Schrodinger ZHU Yifan]

I wonder if we can also have a DSL for benchmark similar to google/benchmark or criterion-rs

[Henrik Böving]

sure, in general I would claim Lean's DSL capabilities are strictly stronger than what is possible in rust

[Henrik Böving]

With large parts of a functioning software eco system for Lean the question is IMO not "can we do it" but rather "where is the person willing to do it" :)

[MangoIV]

There’s tasty-bench so I’d say yes

[Henrik Böving]

Now with property tests! https://github.com/hargoniX/nest-slimcheck

import NestCore
import NestSlimCheck

open Nest.Core
open Nest.SlimCheck

def tests : TestTree := [nest|
  group "examples"
    group "examples positive"
      test "rfl" : PropTest := .mk <| ∀ (x : Nat), x = x
      test "reverse_append" : PropTest := .mk <| ∀ (xs ys : List Nat), (xs ++ ys).reverse = ys.reverse ++ xs.reverse
    group "examples negative"
      test "lt" : PropTest := .mk <| ∀ (x y : Nat), x < y
      test "append_com" : PropTest := .mk <| ∀ (xs ys : List Nat), xs ++ ys = ys ++ xs
]

def main : IO UInt32 := Nest.Core.defaultMain tests

Running group examples:
  Running group examples positive:
    rfl: Unable to find counter examples (seed : 17067480472798704719) [OK]
    reverse_append: Unable to find counter examples (seed : 411235305205085820) [OK]
  Running group examples negative:
    lt: Found a counter example (seed : 13691387637133543223) [FAIL]
      x := 0, y := 0, issue: 0 < 0 does not hold
    append_com: Found a counter example (seed : 10601116111013419514) [FAIL]
      xs := [0], ys := [1], issue: [0, 1] = [1, 0] does not hold

[James Gallicchio]

now to write a fuzzer macro :big_smile:

[Schrodinger ZHU Yifan]

seems hard to make it coverage guarded with C backend (not sure

[Henrik Böving]

Schrodinger ZHU Yifan said:

seems hard to make it coverage guarded with C backend (not sure

I don't think so. We could in theory use coverage tools made by C people. That said once the LLVM backand goes live as the default code generation facility we can use LLVMs coverage mechanism which should make this even nicer for us I believe

[Henrik Böving]

Using built-in C coverage tools will certainly always have an issue though. There are branches that might simply be impossible to hit with common tests without thinking a lot about stuff. For example the uniqueness checks by the RC optimizations. If you write performant code you will always want those to say stuff is unique so it is imaginable you will not hit the false branch. That's why having an LLVM based approach could be quite helpful I think