ucsd-progsys/liquidhaskell

Improve robustness of negative (and positive) tests

Open

#1,661 opened on 2020年5月6日

GitHub で見る
 (2 comments) (1 reaction) (0 assignees)Haskell (1,306 stars) (157 forks)batch import
enhancementgood first issue

説明

Currently most of the neg tests only check that liquid returns an exit code different than 0, but that is usually not enough, because the process might still exit with an error code but for reasons that are not the one we want to test for.

A possible solution is to extend the testsuite to always check for a particular error message. We do this for some tests, but not all, and probably we should be stricter about this.

Conversely, pos tests also suffers from a "generality" problem. We have seen in the past that due to some update in the GHC API, we had tests which were still passing because LH was silently dropping some refinement and thus passing no constraints to the solver.

We discussed possible solutions for this and one of the cheapest option would be to print out the number of generated constraints, so that we could, at least, check that this number is greater than 0, to be sure LH is "doing some work".

コントリビューターガイド