ucsd-progsys/liquidhaskell

Improve robustness of negative (and positive) tests

Open

#1,661 建立於 2020年5月6日

在 GitHub 查看
 (2 留言) (1 反應) (0 負責人)Haskell (1,306 star) (157 fork)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".

貢獻者指南

Improve robustness of negative (and positive) tests · ucsd-progsys/liquidhaskell#1661 | Good First Issue