ucsd-progsys/liquidhaskell

Improve robustness of negative (and positive) tests

Open

#1 661 ouverte le 6 mai 2020

Voir sur GitHub
 (2 commentaires) (1 réaction) (0 assignés)Haskell (157 forks)batch import
enhancementgood first issue

Métriques du dépôt

Stars
 (1 306 stars)
Métriques de merge PR
 (Merge moyen 2j 18h) (12 PRs mergées en 30 j)

Description

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".

Guide contributeur