"(exhausted)" is printed late?

[jwaldmann]

this is nit-picking, but ..

ghci> checkFor 2 $ \ x -> x == not (not x)
+++ OK, passed 2 tests.

ghci> checkFor 3 $ \ x -> x == not (not x)
+++ OK, passed 2 tests (exhausted).

I was expecting the (exhausted) message to appear already in the first example.

[rudymatela]

The meaning of exhausted in LeanCheck is slightly confusing indeed...

I have added (e9f1a89, 5529de1) the following note in the haddock of checkFor clarifying the caveat:

leancheck/src/Test/LeanCheck/IO.hs

Lines 50 to 54 in 5529de1

	-- 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).

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:

1. when configured to test n elements, always try to enumerate n+1, so we know that we are actually exhausted on n;
2. document the caveat to note that exhausted only appears when LeanCheck tries to enumerate but it cannot. That is, when the maximum number of tests is larger than the number of enumerated values.

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: e9f1a89, 5529de1.