Closed jwaldmann closed 2 years ago
The meaning of exhausted in LeanCheck is slightly confusing indeed...
I have added (e9f1a8909ed4ff922333171247b54d13b7f50108, 5529de172d61eb85c9d8e2d1b349ce1d165aa000) the following note in the haddock of checkFor
clarifying the caveat:
Test exhaustion is reported when the configured number of tests is larger than the number of available test values:
> checkFor 3 $ \p -> p == not (not p) +++ OK, passed 2 tests (exhausted).
The straightorward meaning of exhausted would be to say that all possible values are tested. Unfortunately, that is not the case in LeanCheck: here "exhaustion" means: no more tests could be enumerated.
The problem is that there is no way for LeanCheck to know that tests are exhausted unless it tries to enumerate one more element. In your example here:
> checkFor 2 $ \ x -> x == not (not x)
+++ OK, passed 2 tests.
LeanCheck has no way of knowing that there are only two possible booleans unless it tries (and fails) to enumerate a third.
We are left with two options:
With option 1, we would be inconsistent with the number of tests and enumerated values. With option 2, we have a slightly confusing meaning of "exhausted".
I went with option 2: e9f1a8909ed4ff922333171247b54d13b7f50108, 5529de172d61eb85c9d8e2d1b349ce1d165aa000.
this is nit-picking, but ..
I was expecting the
(exhausted)
message to appear already in the first example.