Test Refactor

[madman-bob]

A refactor of Idris's tests. I've used this approach in my own projects.

Test Utilities

I've created a utility script testutils.sh, which can be imported to provide testing utilities to tests. This helps with consistency, and readability. I've extracted a couple of common patterns here.

For example, instead of $1 --no-banner --console-width 0 --no-color ..., we can just write idris2 ....

Test Directories

Instead of naming the tests explicitly in Main.idr, I've used testsInDir as much as possible. This did require me creating an additional directory layer in the idris2 tests. This should prevent tests being added, without being run.

Indeed, the following tests weren't acutally being run:

• allbackends/evaluator005
• chez/barrier001
• chez/forkjoin001
• node/node014
• idris2/builtin012
• idris2/linear004
• racket/forkjoin001
• racket/conditions006
• racket/conditions007

For each of these tests, if it was easy to get the test running, I did so. I've deleted linear004, as it requires linearity subtyping. I'm considering also deleting evaluator005, unless we can decide how Doubles should behave.

Backwards Compatibility

This change will cause merge conflicts with some outstanding PRs. If a PR adds a new test, it will likely cause a conflict in the testing Main.idr. We can throw away their change here, as the testsInDir will pick up the test instead.

If the test is added to the idris2 folder, it should be moved to the appropriate subdirectory.

It is not required to use testutils in any new test, but I reommend importing it if just for the readability improvement over $1 .... Usages of $1 should probably be replaced with one of idris2, $idris2, check, or run.

[gallais]

Cf. discussion in #1736

Edit: I guess now that testsInDir does take a predicate I'm not as opposed to
using it more extensively.