Idris-dev/test
2018-01-25 11:34:39 +00:00
..
base001 Add support for running tests on OpenBSD, fixes #3964 2017-08-04 08:14:38 -07:00
basic001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
basic003 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic004 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic006 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
basic007 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic008 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
basic009 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
basic010 updated the test output 2016-10-12 20:33:07 +00:00
basic011 since BitsN is unsigned through the definition, unsigned operations like prim__udivB8 and 2016-08-04 00:02:45 +08:00
basic012 Normalise type when introducing lambda 2016-03-25 20:53:33 +00:00
basic013 Fix tests for ASCII characters in RTS (#3767) 2017-10-16 11:26:33 +02:00
basic014 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic015 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
basic016 Put source code before error (like parse errors) 2017-12-07 10:18:05 -05:00
basic017 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
basic018 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
basic019 Fix enumFromThenTo 2016-12-09 17:03:32 +01:00
basic020 Expose @ patterns to where functions (#4057) 2017-09-13 16:35:45 +02:00
basic021 added c test using modifyIORef' 2017-10-06 18:53:53 +01:00
basic022 added javascript test for IORef 2017-10-06 08:40:17 +01:00
basic023 Allow declaring fixity of ticked operators (#4140) 2017-10-23 13:09:42 +02:00
basic024 Remove backend tests from input file and into source 2017-10-23 10:15:44 +02:00
basic025 Use native atan2 function from backend 2017-11-03 17:18:36 +01:00
bignum001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
bignum002 Fix generation of bignum literals 2017-10-24 09:41:58 +02:00
bounded001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
buffer001 Fix allocation of buffer 2017-05-24 10:40:51 +02:00
buffer002 Fix tests (buffer002, regression002) 2018-01-22 13:23:14 +00:00
contrib001 Add a test to demonstrate fix of PrettyPrint performance. 2017-11-09 11:25:47 +00:00
corecords001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
corecords002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
delab001 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
directives001 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
directives002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
directives003 Pass directives to C backend in given order (#4078) 2017-10-03 12:31:21 +02:00
disambig002 Add missing test families in test/README.md 2016-07-27 14:45:51 +02:00
docs001 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
docs002 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
docs003 Prelude: implement Functor for Pair a 2017-04-10 12:29:01 -04:00
docs004 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
docs005 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
docs006 Print interface constraints as a separate section 2016-10-12 07:44:33 +02:00
dsl001 Fix name decoration 2017-03-31 14:16:02 +01:00
dsl002 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
dsl003 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
dsl004 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
effects001 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
effects002 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
effects003 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
effects004 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
effects005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
error001 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error002 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
error003 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
error004 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error005 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error006 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error007 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error008 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
error009 Fix error message for unsuccessful namespace disambiguation 2016-08-11 15:29:13 +02:00
ffi001 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
ffi002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
ffi003 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
ffi004 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
ffi005 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
ffi006 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
ffi007 Prefix for pasting in identifiers in C FFI 2017-11-23 20:04:51 +01:00
ffi008 Make type of withAlloc more general 2017-09-22 11:26:34 +02:00
ffi009 Added test for incorrect FFI C usage. 2016-09-15 10:15:53 +01:00
ffi010 added a test for javascript ffi passing functions 2017-06-12 20:57:58 +01:00
ffi011 fixed point free functions, IO returning functions and added a test, all for js interfaces functionality 2017-09-19 19:06:33 +01:00
folding001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
idrisdoc001 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc002 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc003 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc004 replace code level class symbol with inferface 2016-08-27 17:59:43 +08:00
idrisdoc005 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc006 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc007 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc008 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
idrisdoc009 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive001 Indentation configuration via command line args. 2017-01-13 15:27:30 +10:00
interactive002 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive003 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive004 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive005 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive006 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive007 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive008 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive009 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive010 Improve error message locations (#4210) 2017-11-30 12:18:36 +01:00
interactive011 Indentation configuration via command line args. 2017-01-13 15:27:30 +10:00
interactive012 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive013 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interactive014 Add test for :exec (+ fix for test/README.md) 2017-05-14 18:56:32 +08:00
interactive015 Add tests for interactively adding a missing clause 2017-06-20 00:36:04 +02:00
interactive016 Add tests for interactively adding a missing clause 2017-06-20 00:36:04 +02:00
interactive017 Enable test interactive017. 2017-09-03 15:04:08 +10:00
interactive018 Improve interactive018. 2017-09-08 19:46:34 +10:00
interfaces001 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
interfaces002 Reorganise interface elaboration 2017-01-25 19:09:53 +00:00
interfaces003 More control over resolving named implementations 2016-05-08 18:42:53 +01:00
interfaces004 Search open instances first 2016-05-08 20:07:44 +01:00
interfaces005 Change meaning of 'data' in interfaces 2017-03-24 18:54:50 +00:00
interfaces006 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
interfaces007 Deal with interfaces in totality differently 2017-02-21 23:30:36 +00:00
interfaces008 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
interfaces009 Add CHANGELOG entry and test 2017-11-08 21:10:01 +01:00
interpret001 Interpreter tests (#3747) 2017-04-18 08:54:17 +02:00
interpret002 Interpreter tests (#3747) 2017-04-18 08:54:17 +02:00
io001 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
io002 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
io003 prim__vm needs to take a World reference 2016-08-29 18:32:08 -04:00
layout001 Use iWarn for parse errors 2017-12-11 11:52:24 -05:00
literate001 Compose Docs 2017-12-07 11:17:06 -05:00
meta001 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
meta002 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
meta003 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
meta004 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
pkg001 Introduce a PkgName abstraction to represent package name instead of String 2017-10-10 06:27:54 +01:00
pkg002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
pkg003 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
pkg004 Fix test for Windows path separators 2017-11-02 12:43:17 -04:00
pkg005 Better handling of optional main in package files 2016-08-03 07:11:26 +02:00
pkg006 Better handling of optional main in package files 2016-08-03 07:11:26 +02:00
pkg007 Add a test for #3397 2016-09-09 14:07:30 -07:00
pkg008 Updated CHANGELOG and tests. 2017-03-24 09:00:14 +00:00
prelude001 make lines and unlines agree with Haskell 2016-08-04 18:37:38 +08:00
primitives001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
primitives002 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
primitives003 add test cases verifying new verbatim string behavior 2017-11-16 17:54:03 -06:00
primitives004-disabled make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
primitives005 Bump test number. 2016-02-12 10:21:52 +00:00
primitives006 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
proof001 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
proof002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
proof003 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
proof004 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
proof005 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
proof006 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
proof007 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
proof008 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
proof009 Fix name decoration 2017-03-31 14:16:02 +01:00
proof010 Change Instance to implementation (#3404) 2016-09-10 21:06:44 +02:00
proof011 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
proofsearch001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
proofsearch002 prim__vm needs to take a World reference 2016-08-29 18:32:08 -04:00
proofsearch003 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
pruviloj001 Get rid of warnings in pruviloj test 2017-10-04 07:39:20 -04:00
quasiquote001 Normalise embedded paths in normalise. 2016-08-05 11:24:10 +10:00
quasiquote002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
quasiquote003 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
quasiquote004 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
quasiquote005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
quasiquote006 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
records001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
records002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
records003 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
records004 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
records005 Record update by function application 2016-07-04 16:55:15 +01:00
reg001 Take some more care with forcing 2017-03-14 14:32:16 +00:00
reg002 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
reg004 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg005 Added test for unsafePerformIO 2016-01-29 23:23:16 +00:00
reg007 Consolidate reg007 into regression002 2016-08-07 20:36:34 +10:00
reg013 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg016 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg017 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
reg020 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg024 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg025 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg027 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
reg029 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg031 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg032 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg039 Fix reg039 2016-08-27 09:37:37 -04:00
reg040 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
reg041 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
reg042 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg045 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg048 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
reg051-disabled make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg052 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
reg067 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
reg075 Set "--port none" in tests 2016-09-28 00:48:33 +02:00
reg076 Add a regression test. 2016-11-21 12:48:10 +00:00
reg077 Add regression test for #3651. 2017-03-16 12:21:32 -04:00
regression001 Fix implicits under rewrite 2017-03-25 20:18:37 +00:00
regression002 Add mysteriously missing bits of regression002 2018-01-25 11:34:39 +00:00
regression003 Merge branch 'master' of github.com:idris-lang/Idris-dev into add_regression_test_js_unexpected_con_as_glob 2017-07-22 09:26:41 +01:00
scripts Move timeout from test/bin/ to test/scripts/ 2016-08-07 21:35:42 +10:00
sourceLocation001 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
st001 Updated comments according to review comments: 2017-12-05 21:33:42 +01:00
st002 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
st003 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
st004 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
st005 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
st006 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
st007 First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
sugar001 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
sugar002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
sugar003 Purify Idris of "return" 2016-08-27 08:26:45 -04:00
sugar004 Update the test for let- and bind-alternatives 2017-12-22 07:26:52 +01:00
sugar005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
syntax001 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
syntax002 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
tactics001 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
totality001 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality003 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality004 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
totality006 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality007 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality008 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality009 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
totality010 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality011 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality012 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality013 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality014 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
totality015 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality016 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality017 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality018 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality019 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality020 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality021 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality022 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality023 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
totality024 Add test for totality checking of partially applied function 2017-11-15 18:28:20 +01:00
tutorial001 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
tutorial002 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
tutorial003 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
tutorial004 Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
tutorial005 make the tests respect the IDRIS env variable 2016-01-22 06:57:04 +01:00
tutorial006 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
tutorial007 Fix formatting of some tests 2016-07-27 14:33:50 +02:00
unique001 Hide more features behind %language pragmas 2016-12-07 19:38:08 +00:00
unique004 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
universes001 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
universes002 Don't include '=' for RHS span 2017-12-07 10:18:08 -05:00
views001 fix broken tests caused by mod precedence 2017-12-11 16:08:22 -06:00
views002 fix broken tests caused by mod precedence 2017-12-11 16:08:22 -06:00
views003 Convention says the function should be 'vList' 2016-04-12 16:43:27 +01:00
mktest.pl Fix warning for implicitable names 2016-02-13 13:27:30 +00:00
README.md First attempt at implementing ST alternative for File.idr in Effects. 2017-11-27 12:05:00 +01:00
TestData.hs Add some buffer primitives 2017-12-29 18:44:01 +00:00
TestRun.hs Unused imports 2017-09-19 14:33:41 -04:00

Idris' Testing Suite

Running the test suite

Do make test_c or make test_js. It will run the tests in parallel and through cabal test. You can also manually call cabal test or stack test.

Passing arguments

To the test program

You can pass arguments to the test program. For example, to pass the --help argument:

# Via make
make TEST-ARGS="--help" test_c
# Via cabal
cabal test --test-options="--help"
# Via stack
stack test --test-arguments="--help"

Try it to learn more about the other arguments you can provide. Two are of particular interest: --node to test against the Node code generator and --pattern <regex> to only run the test that match the provided <regex>.

To idris

You can pass arguments to idris in each of its invocation by the tests. There are two ways to this. You can either modify the idrisFlags term in TestRun, or set the $IDRIS environment variable accordingly

Specifying the number of parallel jobs

With make, the test suite runs in parallel by default. You can specify the number of threads with TEST-JOBS. For stack and cabal, you need to explicitly enable parallelism as you would do with any other GHC-compiled executable. Examples:

# Two test jobs via make
make TEST-JOBS=2 test_c
# Two test jobs via cabal
cabal test --test-options="+RTS -N2 -RTS"
# Two test jobs via stack
stack test --test-arguments="+RTS -N2 -RTS"

Running only previously failed tests

Because of the --rerun-update option, make test_c will create a .tasty-rerun-log file in the root directory of the project. Each time the test suite is run, the file will be written with the result of the tests. The next time you do make test, you can specify the rerun-filter argument to, for example, only run previously failed tests. Valid values are given in the --help.

Extending the test suite

Content of the directory

To each test there shall be a folder that holds at least a bash script run and a golden file expected. When running the test suite, the standard output of the script is compared against the golden file. Any mismatch is reported as a failure.

The name of a test folder is the identifier of the test family followed by a three digit number. A test family gathers related tests.

Add to that four top level files:

  • The program TestRun.hs that runs the test suite
  • A Haskell module TestData.hs with the metadata for each test
  • The Perl script mktest.pl to ease the creation of a new test
  • This README.md

Test families

Tests are categorised with the following test families (and their identifiers):

  • basic: Basic language features, some complete programs
  • bignum: Bignums and GMP
  • bounded: Bounds testing for bits
  • corecords: Tests for corecord
  • delab: De-elaboration tests
  • directives: Tests for directives
  • disambig: Disambiguaton tests
  • docs: Testing documentation functionality
  • dsl: Embedded DSLs and features to support DSL development
  • effects: Effects package
  • error: Error messages and error reflection
  • ffi: FFI calls, including type providers
  • folding Testing some folds
  • idrisdoc: Documentation tool functionality
  • interactive: Interactive editing, proof search
  • interfaces: Testing interfaces.
  • io: IO monad
  • literate: .lidr files; literate programming
  • meta: Meta-programming
  • pkg: Packages
  • primitives: Primitive types
  • proof: Theorem proving, tactics
  • proofsearch: Proof search
  • pruviloj: Elaborator reflection
  • quasiquote: Quasiquotations
  • records: Records
  • reg: Regression tests, covering previous bug fixes
  • regression: Regression tests, covering previous bug fixes
  • sourceLocation: Interaction with files from Idris
  • st: ST, state transition systems
  • sugar: Syntactic sugar, syntax extensions
  • syntax: Syntax extensions
  • tactics: Testing for tactics
  • totality: Totality checking
  • tutorial: Examples from the tutorial
  • unique: Uniqueness types
  • universes: Universes
  • views: Views and covering functions

Adding a test family

  1. Choose an available identifier for your test family. It should be short and somewhat self-explanatory.
  2. Add it in the README.md file, i.e. just above.
  3. Add it in TestData.hs, in the testFamiliesData list. Say the chosen identifier is foo. You should append to the list ("foo", "A proper name for foo", [ ]). The empty list will be replaced with the metadata of each test in the family.
  4. Add your tests.

Adding a test

  1. Choose the family your test shall belong to and remember its identifier.
  2. Pick the next available integer in the test family. It will be the index.
  3. Say the family's identifier is foo and the index is 42. You should call ./mktest.pl foo042 ; this will create the directory and a simple run script.
  4. Modify the run script to your liking. If you want to call the idris executable, write ${IDRIS:-idris} $@.
  5. Add any file you may need in the directory. If they don't end in .idr, you should remember them for the next step.
  6. Add your test in TestData.hs. Each family has a list of (Index, CompatCodegen). See the next section for the available values in CompatCodegen. In most cases, you should write ( 42, ANY).
  7. Generate the expected file by doing:
    # Using cabal
    cabal test --test-options="--pattern foo042 --accept"
    # Using stack
    stack test --test-arguments="--pattern foo042 --accept"
    
  8. Check the content of expected. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

Specifying compatible backends

Some tests only make sense with specific code generators. Others don't generate code. You need to supply this information in testFamiliesData. Available values for the compatible backends are:

  • ANY: choose this if your test will work with any code generator
  • C_CG: choose this to only test against the C code generator
  • NODE_CG: choose this to only test against the Node code generator
  • NONE: choose this if you don't want your test to be run with multiple code generators (mainly for tests that only perform type checking)

Currently, NONE has the same effect as ANY, but this will change.

Removing a test

  1. Delete the corresponding directory
  2. Remove the corresponding line in the definition of testFamiliesData in TestData.hs

Updating golden files

To update the expected file for every test, do one of the following:

# Using make
make test_update
# Using cabal
cabal test --test-options="--accept"
# Using stack
stack test --test-arguments="--accept"

"Accepted" tests are the ones that update the golden file. A test can still fail if the run script itself crashes.