on d552eef help sign in
Idris-dev/test
218 folders, 4 files
../ base001/Reverted changes to verbosity reporting. basic001/make the tests respect the IDRIS env variable basic002/Remove redundant --consolewidth settings in tests basic003/make the tests respect the IDRIS env variable basic004/make the tests respect the IDRIS env variable basic005/make the tests respect the IDRIS env variable basic006/Don't query width when not a tty basic007/make the tests respect the IDRIS env variable basic008/Purify Idris of "return" basic009/Don't query width when not a tty basic010/updated the test output basic011/since BitsN is unsigned through the definition, unsigned operations like prim__udivB8 and prim__uremB8 should be used rather than the signed ones basic012/Normalise type when introducing lambda basic013/Updating range behavior to match Haskell's where appropriate basic014/make the tests respect the IDRIS env variable basic015/make the tests respect the IDRIS env variable basic016/Remove redundant --consolewidth settings in tests basic017/Remove redundant --consolewidth settings in tests basic018/Revert to normalising from WHNF basic019/Fix enumFromThenTo bignum001/make the tests respect the IDRIS env variable bignum002/make the tests respect the IDRIS env variable bounded001/make the tests respect the IDRIS env variable buffer001/Add Data.Buffer corecords001/make the tests respect the IDRIS env variable corecords002/make the tests respect the IDRIS env variable delab001/Set "--port none" in tests directives001/Don't query width when not a tty directives002/Added test case directive002 disambig002/Add missing test families in test/README.md docs001/Set "--port none" in tests docs002/Set "--port none" in tests docs003/Set "--port none" in tests docs004/Set "--port none" in tests docs005/Set "--port none" in tests docs006/Print interface constraints as a separate section dsl001/Support interfaces in mutual blocks dsl002/Hide more features behind %language pragmas dsl003/Hide more features behind %language pragmas dsl004/Hide more features behind %language pragmas effects001/Purify Idris of "return" effects002/Purify Idris of "return" effects003/Remove redundant --consolewidth settings in tests effects004/make the tests respect the IDRIS env variable effects005/make the tests respect the IDRIS env variable error001/Store file with constraints + export error002/Purify Idris of "return" error003/Purify Idris of "return" error004/Purify Idris of "return" error005/'compute' rather than whnf on disambiguation error006/Remove redundant --consolewidth settings in tests error007/Lazy elaboration tweaks error008/Don't use top level elab for resolveTC error009/Fix error message for unsuccessful namespace disambiguation ffi001/Set "--port none" in tests ffi002/Set "--port none" in tests ffi003/Set "--port none" in tests ffi004/Set "--port none" in tests ffi005/Purify Idris of "return" ffi006/Purify Idris of "return" ffi007/Purify Idris of "return" ffi008/Purify Idris of "return" ffi009/Added test for incorrect FFI C usage. folding001/make the tests respect the IDRIS env variable idrisdoc001/Fix formatting of some tests idrisdoc002/Fix formatting of some tests idrisdoc003/Fix formatting of some tests idrisdoc004/replace code level class symbol with inferface idrisdoc005/Fix formatting of some tests idrisdoc006/Fix formatting of some tests idrisdoc007/Fix formatting of some tests idrisdoc008/Fix formatting of some tests idrisdoc009/Set "--port none" in tests interactive001/Indentation configuration via command line args. interactive002/Set "--port none" in tests interactive003/Set "--port none" in tests interactive004/Set "--port none" in tests interactive005/Set "--port none" in tests interactive006/Set "--port none" in tests interactive007/Set "--port none" in tests interactive008/Set "--port none" in tests interactive009/Set "--port none" in tests interactive010/Another scoped implicit fix interactive011/Indentation configuration via command line args. interactive012/Set "--port none" in tests interactive013/Set "--port none" in tests interfaces001/Set "--port none" in tests interfaces002/Reorganise interface elaboration interfaces003/More control over resolving named implementations interfaces004/Search open instances first interfaces005/Change meaning of 'data' in interfaces interfaces006/Purify Idris of "return" interfaces007/Deal with interfaces in totality differently io001/Purify Idris of "return" io002/Purify Idris of "return" io003/prim__vm needs to take a World reference layout001/Set "--port none" in tests literate001/Remove redundant --consolewidth settings in tests meta001/Hide more features behind %language pragmas meta002/Hide more features behind %language pragmas meta003/Hide more features behind %language pragmas meta004/Hide more features behind %language pragmas pkg001/Allowed `--highlight` in pkg commands. pkg002/make the tests respect the IDRIS env variable pkg003/make the tests respect the IDRIS env variable pkg004/make the tests respect the IDRIS env variable pkg005/Better handling of optional main in package files pkg006/Better handling of optional main in package files pkg007/Add a test for #3397 pkg008/Updated CHANGELOG and tests. prelude001/make lines and unlines agree with Haskell primitives001/make the tests respect the IDRIS env variable primitives002/Set "--port none" in tests primitives003/make the tests respect the IDRIS env variable primitives004-disabled/make the tests respect the IDRIS env variable primitives005/Bump test number. primitives006/Purify Idris of "return" proof001/Make Vect follow the naming convention of List proof002/Hide more features behind %language pragmas proof003/Purify Idris of "return" proof004/Fix formatting of some tests proof005/Fix formatting of some tests proof006/Fix formatting of some tests proof007/Fix formatting of some tests proof008/Fix formatting of some tests proof009/Set "--port none" in tests proof010/Change Instance to implementation (#3404) proof011/Don't query width when not a tty proofsearch001/make the tests respect the IDRIS env variable proofsearch002/prim__vm needs to take a World reference proofsearch003/Fix formatting of some tests pruviloj001/Hide more features behind %language pragmas quasiquote001/Normalise embedded paths in `normalise`. quasiquote002/make the tests respect the IDRIS env variable quasiquote003/Don't query width when not a tty quasiquote004/Remove redundant --consolewidth settings in tests quasiquote005/make the tests respect the IDRIS env variable quasiquote006/Set "--port none" in tests records001/make the tests respect the IDRIS env variable records002/make the tests respect the IDRIS env variable records003/make the tests respect the IDRIS env variable records004/make the tests respect the IDRIS env variable records005/Record update by function application reg001/Take some more care with forcing reg002/Fix formatting of some tests reg004/make the tests respect the IDRIS env variable reg005/Added test for unsafePerformIO reg007/Consolidate reg007 into regression002 reg013/make the tests respect the IDRIS env variable reg016/make the tests respect the IDRIS env variable reg017/Remove redundant --consolewidth settings in tests reg020/make the tests respect the IDRIS env variable reg024/make the tests respect the IDRIS env variable reg025/make the tests respect the IDRIS env variable reg027/Don't query width when not a tty reg029/make the tests respect the IDRIS env variable reg031/make the tests respect the IDRIS env variable reg032/make the tests respect the IDRIS env variable reg039/Fix reg039 reg040/Purify Idris of "return" reg041/Set "--port none" in tests reg042/make the tests respect the IDRIS env variable reg045/make the tests respect the IDRIS env variable reg048/Purify Idris of "return" reg051-disabled/make the tests respect the IDRIS env variable reg052/Purify Idris of "return" reg067/make the tests respect the IDRIS env variable reg075/Set "--port none" in tests reg076/Add a regression test. reg077/Add regression test for #3651. regression001/Fix implicits under rewrite regression002/Modify pretty printer for lambdas scripts/Move `timeout` from `test/bin/` to `test/scripts/` sourceLocation001/Hide more features behind %language pragmas sugar001/make the tests respect the IDRIS env variable sugar002/make the tests respect the IDRIS env variable sugar003/Purify Idris of "return" sugar004/make the tests respect the IDRIS env variable sugar005/make the tests respect the IDRIS env variable syntax001/Don't query width when not a tty syntax002/make the tests respect the IDRIS env variable tactics001/Hide more features behind %language pragmas totality001/Don't query width when not a tty totality002/Don't query width when not a tty totality003/Fix formatting of some tests totality004/Don't query width when not a tty totality005/make the tests respect the IDRIS env variable totality006/Don't query width when not a tty totality007/make the tests respect the IDRIS env variable totality008/Don't query width when not a tty totality009/Fix formatting of some tests totality010/Don't query width when not a tty totality011/updated the test output totality012/Look under if...then...else in totality checker totality013/Change totality checking and inlining totality014/Small reduction in constraint generation totality015/Change totality checking and inlining totality016/Make totality checker to report partial functions correctly (fix #2884) totality017/Make totality checker to report partial functions correctly (fix #2884) totality018/Look deeper when coverage checking totality019/New coverage checker totality020/Use conversion errors in coverage check totality021/Deal with ambiguity in impossible clauses totality022/Fix a proof of Void tutorial001/Fix formatting of some tests tutorial002/Remove redundant --consolewidth settings in tests tutorial003/make the tests respect the IDRIS env variable tutorial004/Remove redundant --consolewidth settings in tests tutorial005/make the tests respect the IDRIS env variable tutorial006/Make Vect follow the naming convention of List tutorial007/Fix formatting of some tests unique001/Hide more features behind %language pragmas unique004/Hide more features behind %language pragmas universes001/Store file with constraints + export universes002/Small reduction in constraint generation views001/Add Data.Vect.Views views002/Fix views tests on node backend views003/Convention says the function should be 'vList' README.mdRemove irreleveant line from test README TestData.hsAdd Data.Buffer TestRun.hsAlso look for nodejs in addition to node in the testsuite mktest.plFix warning for implicitable names