Idris2/tests
Steve Dunham b944062137
[ fix ] Address some proofs of void via impossible from issues #2250 and #3276 (#3396)
* [ fix ] impossible confuses constructors between types

* Handle IAlternative when making an impossible term

* Check types in impossible clauses
2024-11-22 22:38:54 -05:00
..
allbackends [ fix ] Support waiting for popen2-created processes 2023-12-19 23:03:31 +03:00
allschemes [ performance ] Implement weak memoisation of lazy values for chez and racket (#2791) 2024-08-06 15:24:57 +01:00
base idris_support: fix environ for macOS (#3324) 2024-07-03 12:04:22 -05:00
chez [ base ] Add atomically function (#3380) 2024-09-11 09:18:47 +01:00
codegen [ codegen ] get rid of artifacts introduced when optimizing IO (#3376) 2024-08-26 11:30:09 +01:00
contrib Add JSON manipulation functions 2024-06-25 10:37:18 -05:00
gambit/bitops001 Add testing utilities script 2023-09-07 14:57:22 +01:00
ideMode Emit warning for fixities with no export modifiers (#3234) 2024-04-03 15:41:57 +01:00
idris2 [ fix ] Address some proofs of void via impossible from issues #2250 and #3276 (#3396) 2024-11-22 22:38:54 -05:00
linear/system_concurrency_session [ new ] System.Concurrency.(Linear/Session) (#3294) 2024-06-05 13:53:30 +01:00
node Add %foreign_impl pragma for augmenting ffi functions (#3303) 2024-06-11 17:45:09 +01:00
prelude Add pipeline operators (#3284) 2024-06-06 10:59:30 +01:00
racket [ performance ] Implement weak memoisation of lazy values for chez and racket (#2791) 2024-08-06 15:24:57 +01:00
refc [RefC] Object Immortalization and Pre-Generation of Constants (#3242) 2024-11-20 17:15:26 -06:00
templates Add testing utilities script 2023-09-07 14:57:22 +01:00
ttimp Revert "[ new ] totality checking can look under constructors (#3328)" 2024-07-26 14:45:54 +01:00
typedd-book WithFC, a datastructure to keep track of locations (#3406) 2024-11-08 08:43:53 +09:00
vmcode/basic001 Add testing utilities script 2023-09-07 14:57:22 +01:00
Main.idr [ fix ] case spliting under implicit/auto parameter 2024-06-13 08:40:33 +01:00
Makefile Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
README.md [ re #2649 ] Describe test naming pattern 2022-11-11 09:33:09 +01:00
tests.ipkg Set PREFIX for tests 2021-04-19 11:23:58 +01:00
testutils.sh Fix annoying warning when running tests on some macOS machines (#3346) 2024-07-08 09:27:29 +01:00

Tests

Note: The commands listed in this section should be run from the repository's root folder.

Run all tests: make test

To run only a subset of the tests use: make test only=NAME. NAME is matched against the path to each test case.

Examples:

  • make test only=chez will run all Chez Scheme tests.
  • make test only=ttimp/basic will run all basic tests for TTImp.
  • make test only=idris2/basic001 will run a specific test.

Templates for common test instances can be found in the templates folder.

There is no defined naming convention for adding tests, but the pattern has been:

  • a sub-directory in the relevant test section (idris2, refc, etc.)
  • with a descriptive name followed by a 3-digit number (e.g. envflags001 is the first test checking the environment flags functions)
  • containing:
    • an Idris file importing the relevant modules and containing the test function(s)
    • a run file which is a shell script that runs the test (see the existing tests for examples for this)
    • an expected file containing the expected output