An Idris port of the Haskell Hedgehog library, a property-based testing library in the spirit of QuickCheck.
This is still work in progress but the core functionality is already there and a tutorial is in the making.
-
Monadic random value generators with integrated shrinking.
-
Numeric ranges with well-defined scaling and shrinking behavior.
-
Colorized test output with pretty printing of value diffs in case of failed tests (right now, colorize output has to be enabled by setting environment variable
HEDGEHOG_COLOR="1"). -
Conveniently define generators for regular algebraic data types via their generic representations as sums of products (see idris2-sop).
-
Provably total core: While the Haskell library allows us to define (and consume) infinite shrink trees, this is not possible here due to the codata nature of the trees we use for shrinking.
-
Classify generated values and verify test coverage.
-
No filtering of generators: In my experience, generators should create random values constructively. Filtering values makes it too easy to write generators, the combination of which fails most of the time.
-
Genis not a monad transformer right now, therefore it cannot be combined with additional monadic effects. The main reason for this is that we use aCotreecodata type for shrinking, and it is hard to combine this with monadic effects in a provably total way. -
No support for state machine testing (yet).
-
No automatic detection of properties in source files (yet).
-
No parallel test execution (yet).
There are two main differences: First, there is no Arbitrary interface
and therefore, generators have typically to be hand-written. However, using
a sums of products approach (tutorial yet to be added) makes
it very easy to write generators for regular algebraic data types.
Second, shrinking is integrated, which makes it very easy to write
generators with good shrinking behavior, especially when using
an applicative style for writing generators, in which case shrinking
is completely free
(see also integrated vs manual shrinkig).
Starting from Idris2 version 0.5.1, tagged releases of the same minor version number (e.g. 0.5.x) will be made available, while the main branch keeps following the Idris2 main branch.
In addition, the following external dependencies are required:
The latest commit is daily tested to build against the current HEAD of the Idris compiler. Since Idris2 releases are happening rather infrequently at the moment, it is suggested to use a package manager like pack to install and maintain matching versions of the Idris compiler and this library. Pack will also automatically install all required dependencies.