Mentions légales du service

Skip to content
Snippets Groups Projects

Use QCheck for the random test suite

Merged MARTINOT Olivier requested to merge omartino/inferno:qcheck into master
All threads resolved!

One of the main motivation for this change is that QCheck allows us to use a shrinker, providing more concise counter examples.

Edited by MARTINOT Olivier

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • MARTINOT Olivier added 2 commits

    added 2 commits

    Compare with previous version

  • 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/result and list and shrink only those.)

  • added 1 commit

    • b2a3228a - fixup! Random generation of ML terms using qcheck.

    Compare with previous version

  • MARTINOT Olivier marked this merge request as draft from omartino/inferno@b2a3228a

    marked this merge request as draft from omartino/inferno@b2a3228a

  • MARTINOT Olivier resolved all threads

    resolved all threads

  • The new code has two sort of testing functions, test_with_log (the previous machinery that manually handlers a log) and test (the new code that is driven by QCheck). It would be nice to remove the duplication, but currently test_with_log is 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).

  • MARTINOT Olivier added 3 commits

    added 3 commits

    Compare with previous version

  • MARTINOT Olivier marked this merge request as ready

    marked this merge request as ready

  • Note: we have not yet tried to see if #2 (closed) can be reproduced (and shrunk).

  • SCHERER Gabriel mentioned in commit abf1da90

    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 checksum

    Would you, by any chance, have messed up with the tarball of menhir 2021/04/19 after the submission on opam, changing the tarball checksum?

  • No. There is a problem with gitlab.inria.fr: all archives are now behind an authentication barrier. I have reported the problem.

  • Please register or sign in to reply
    Loading