LSpec

This repo contains a fork of the LSpec Lean testing framework, adapted to work with Lean's Plausible property-based testing library.

Usage

Composing tests

Sequences of tests are represented by the TestSeq datatype. In order to instantiate terms of TestSeq, use the test helper function:

#check
  test "Nat equality" (4 = 4) $
  test "Nat inequality" (4 ≠ 5)
-- test "Nat equality" (4 = 4) (test "Nat inequality" (4 ≠ 5)) : TestSeq

test consumes a description a proposition and a next test The proposition, however, must have its own instance of Testable.

You can also collect TestSeq into conceptual test groups by using the helper function group:

#check
  test "Nat equality" (42 = 42) $
  group "manual group" $
    test "Nat equality inside group" (4 = 4)

The Testable class

Testable is how Lean is instructed to decide whether certain propositions are resolved as true or false.

This is an example of a simple instance for decidability of equalities:

instance (x y : α) [DecidableEq α] [Repr α] : Testable (x = y) :=
  if h : x = y then
    .isTrue h
  else
    .isFalse h s!"Not equal: {repr x} and {repr y}"

The custom failure message is optional.

There are more examples of Testable instances in LSpec/Instances.lean.

The user is, of course, free to provide their own instances.

Actually running the tests

The #lspec command

The #lspec command allows you to test interactively in a file.

Examples:

#lspec
  test "four equals four" (4 = 4) $
  test "five equals five" (5 = 5)
-- ✓ four equals four
-- ✓ five equals five

An important note is that a failing test will raise an error, interrupting the building process.

The lspecIO function

lspecIO is meant to be used in files to be compiled and integrated in a testing infrastructure, as shown below.

def aaSuite := [
    test "four equals four" (4 = 4)
  ]

def bbSuite := [
    test "five equals five" (5 = 5)
  ]

def main := lspecIO $ .ofList [
    ("aa", aaSuite),
    ("bb", bbSuite)
  ]

Once such main function is defined, its respective executable can be tagged as the @[test_driver] in the lakefile. For further information, inspect the docstring of lspecIO.

Integration with Plausible

There are 3 main typeclasses associated with any Plausible property-based test:

• Shrinkable : The typeclass that takes a type a : α and returns a List α of elements which should be thought of as being "smaller" than a (in some sense dependent on the type α being considered).
• SampleableExt : The typeclass of random generators for values of type α. This is roughly equivalent to the Arbitrary` typeclass in Haskell QuickCheck.
• Plausible.Testable : The property to be checked by Plausible must have a Plausible.Testable instance.

In order to use Plausible tests for custom data types, the user will need to implement instances of the typeclasses Shrinkable and SampleableExt for the custom types appearing in the properties being tested.

The Plausible library contains many of the useful definitions and instances that can be used to derive a Plausible.Testable instance for a wide variety of properties given just the instances above. If all else fails, the user can also define the Plausible.Testable instance by hand.

Once this is done, a Plausible test is evaluated in a similar way to LSpec tests:

#lspec check "add_comm" $ ∀ n m : Nat, n + m = m + n

#lspec check "add_comm" $ ∀ n m : Nat, n + m = m + m
-- × add_comm

-- ===================
-- Found problems!
-- n := 1
-- m := 0
-- issue: 1 = 0 does not hold
-- (0 shrinks)
-- -------------------