Use QCheck for the random test suite
One of the main motivation for this change is that QCheck allows us to use a shrinker, providing more concise counter examples.
Merge request reports
Activity
added 2 commits
-
The main difference from the previous random generator is that now we have a shrinker for failing test cases. We played with the shrinker and the current state is reasonable (it's good but not excellent, it shrinks well enough in simple experiments). I have ideas to improve the shrinker by introduced typed holes ( https://gitea.lakaban.net/Olivier/inferno-experimental/issues/32 ), but they could come as a separate MR.
Another thing that we could still improve is: currently the generator more or less matches the behavior of the previous one, it does not cover more language constructs even though we extended the language. (No generator support for variants and pattern-matching). It would be nice to do better. Note that it's not clear how to effectively generate random programs using nominal type declarations, as would be required for datatype and pattern matching. (We could tell the generator about
option/resultandlistand shrink only those.) added 1 commit
- b2a3228a - fixup! Random generation of ML terms using qcheck.
marked this merge request as draft from omartino/inferno@b2a3228a
-
The new code has two sort of testing functions,
test_with_log(the previous machinery that manually handlers alog) andtest(the new code that is driven by QCheck). It would be nice to remove the duplication, but currentlytest_with_logis still used by unit tests (not random tests), and QCheck is not meant to run simple unit tests. We could use a unit-testing framework that meshes well with QCheck (ounit, alcocheck) to remove the home-made logging logic, but it is unclear that we would win that much (shorter code but more complex dependency; nicer output). -
Note: we have not yet tried to see if #2 (closed) can be reproduced (and shrunk).
mentioned in commit abf1da90
-
@fpottier : merging this PR led to a failure in our brand new CI. It's first failure! What an emotional moment.
The logs look like the following:
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ERROR] The sources of the following couldn't be obtained, aborting: - menhir.20210419: Bad checksum - menhirLib.20210419: Bad checksum - menhirSdk.20210419: Bad checksumWould you, by any chance, have messed up with the tarball of menhir 2021/04/19 after the submission on opam, changing the tarball checksum?
