Framework for testing at runtime

Stream: general

[Oliver Dressler]

I have been enjoying runtime Lean but miss a more streamlined testing experience.
Users of runtime Lean, what have you been using for testing?

After some planning, I want to implement the following API to fit my needs.
Would this also fit your projects? Any oversights, name collisions, or additions?

Test Definition

import LeanTest

-- BASIC TESTING
#test_eq "named test": a b "custom error message"
#test_eq a b
#test_ne a b
#test_true condition
#test_false condition

-- GROUPING
#test_group "name" do
  -- tests

-- PROPERTY TESTING
#test_forall (cases? := n) (seed? := m) (generator? := custom_gen) (x : T) => property
#test_forall (generators? := [custom_gen, custom_gen2]) (x : T) (y : U) ... => property

-- EQUALITY ASSERTIONS
#test_eq a b
#test_ne a b
#test_beq a b
#test_bne a b
#test_equiv a b
#test_not_equiv a b

-- ORDERING ASSERTIONS
#test_lt a b
#test_le a b
#test_gt a b
#test_ge a b

-- MEMBERSHIP ASSERTIONS
#test_member x xs
#test_not_member x xs
#test_subset xs ys
#test_not_subset xs ys
#test_divides a b
#test_not_divides a b

-- RELATIONAL ASSERTIONS
#test_rel R a b
#test_not_rel R a b
#test_pred P x
#test_not_pred P x

-- COLLECTION ASSERTIONS
#test_empty collection
#test_not_empty collection
#test_size collection n

-- NUMERIC ASSERTIONS
#test_approx a b ε

-- OPTION ASSERTIONS
#test_some opt
#test_none opt
#test_some_eq opt expected
#test_some_ne opt forbidden
#test_some_lt opt bound
#test_some_le opt bound
#test_some_gt opt bound
#test_some_ge opt bound
#test_some_pred opt predicate
#test_some_not_pred opt predicate

-- EXCEPT ASSERTIONS
#test_ok result
#test_error result
#test_ok_eq result expected
#test_ok_ne result forbidden
#test_ok_lt result bound
#test_ok_le result bound
#test_ok_gt result bound
#test_ok_ge result bound
#test_ok_pred result predicate
#test_ok_not_pred result predicate
#test_error_eq result expected_error
#test_error_ne result forbidden_error
#test_error_pred result error_predicate

-- EXCEPTION TESTING
#test_throws expr
#test_not_throws expr
#test_panic expr

-- PERFORMANCE TESTING
#test_time (runs? := n) (timeout? := ms) expr

-- CONFIGURATION
#test_config do
  cases := n
  ?? parallel := bool
  seed := n

Setup and Execution

[[require]]
name = "LeanTest"
git = "https://github.com/.../LeanTest"
rev = "main"

testDriver = "LeanTest/driver"

lake test
lake test File.lean
lake test --watch
?? lake test --junit-xml=report.xml

Example Output

MathTests.lean [3 tests, 1 failed]
------------------------------
✗ simple_addition (MathTests.lean:12)
  expected: 5
  actual:   4

AlgebraTests.lean [3 tests, 1 failed]
------------------------------
quadratic_formula [1 test, 1 failed]
  ✗ solve_quadratic (AlgebraTests.lean:27)
    property failed for inputs: x = 0, -1, 2
    smallest failing case: x = 0
    seed: 42
    generator: small_ints

LogicTests.lean [2 tests, 1 failed]
------------------------------
✗ boolean_logic_test (LogicTests.lean:18)
  expected: true
  actual:   false

PerformanceTests.lean [2 tests, 1 failed]
------------------------------
✗ fast_function (PerformanceTests.lean:40)
  test_time exceeded timeout
  measured time: 0.08s (timeout: 0.05s)

time_measurement_example (PerformanceTests.lean:45)
  measured time per call: 0.03s

UtilityTests.lean [2 tests, 0 failed]
------------------------------

10 tests, 3 failed (0.56s)

[Arthur Paulino]

We (argumentcomputer) use LSpec

[Oliver Dressler]

Arthur Paulino said:

We (argumentcomputer) use LSpec

Thanks, somehow I missed this on my (admittedly short) search. LSpec does a lot of what I was missing.
I'm looking through your yatima tests to see it in action now.

[Arthur Paulino]

yatima is no longer maintained and uses an old version of LSpec.
ix serves as a better example