git.iko.soy/Idris-dev
on d86f82e help sign in
Idris-dev/test
258 folders, 4 files
../ base001/Use $CC instead of gcc basic001/make the tests respect the IDRIS env variable basic002/Add blank line after "large" messages 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/Add blank line after "large" messages basic007/make the tests respect the IDRIS env variable basic008/Purify Idris of "return" basic009/Don't include '=' for RHS span 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/Fix tests for ASCII characters in RTS (#3767) basic014/make the tests respect the IDRIS env variable basic015/make the tests respect the IDRIS env variable basic016/Put source code before error (like parse errors) basic017/Add blank line after "large" messages basic018/Don't include '=' for RHS span basic019/Fix enumFromThenTo basic020/Expose `@` patterns to where functions (#4057) basic021/added c test using modifyIORef' basic022/added javascript test for IORef basic023/Allow declaring fixity of ticked operators (#4140) basic024/Remove backend tests from input file and into source basic025/Use native `atan2` function from backend basic026/Fin.restrict fix (#4337) bignum001/make the tests respect the IDRIS env variable bignum002/Fix generation of bignum literals bignum003/Fix looped temporary allocations in mini-GMP (#4324) bounded001/make the tests respect the IDRIS env variable buffer001/Fix allocation of buffer buffer002/Update test buffer002 to use valid Int values on 32-bit builds contrib001/Add a test to demonstrate fix of PrettyPrint performance. 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 include '=' for RHS span directives002/Add blank line after "large" messages directives003/Pass directives to C backend in given order (#4078) disambig002/Make Iso a record docs001/Amended the test suite to report updated documentation. docs002/Amended the test suite to report updated documentation. docs003/Amended the test suite to report updated documentation. docs004/Amended the test suite to report updated documentation. docs005/Amended the test suite to report updated documentation. docs006/Amended the test suite to report updated documentation. dsl001/Fix name decoration dsl002/Fix binding rules in patterns dsl003/Hide more features behind %language pragmas dsl004/Hide more features behind %language pragmas effects001/fix for odd-even bug in random (#4339) effects002/Purify Idris of "return" effects003/fix for odd-even bug in random (#4339) effects004/make the tests respect the IDRIS env variable effects005/make the tests respect the IDRIS env variable error001/Add blank line after "large" messages error002/Purify Idris of "return" error003/Don't include '=' for RHS span error004/Add blank line after "large" messages error005/Add blank line after "large" messages error006/Raise an error if too many "with" arguments are provided error007/Add blank line after "large" messages error008/Add blank line after "large" messages error009/Fix error message for unsuccessful namespace disambiguation ffi001/Set "--port none" in tests ffi002/Add blank line after "large" messages ffi003/Set "--port none" in tests ffi004/Set "--port none" in tests ffi005/Purify Idris of "return" ffi006/Purify Idris of "return" ffi007/Prefix for pasting in identifiers in C FFI ffi008/Make type of `withAlloc` more general ffi009/Added test for incorrect FFI C usage. ffi010/added a test for javascript ffi passing functions ffi011/fixed point free functions, IO returning functions and added a test, all for js interfaces functionality ffi012/fix #4656 ffi013/test for file existence 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/Amended the test suite to report updated documentation. 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/Amended the test suite to report updated documentation. 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/Improve error message locations (#4210) interactive011/Indentation configuration via command line args. interactive012/Set "--port none" in tests interactive013/Set "--port none" in tests interactive014/Add test for :exec (+ fix for test/README.md) interactive015/Add tests for interactively adding a missing clause interactive016/Add tests for interactively adding a missing clause interactive017/Enable test interactive017. interactive018/Improve interactive018. interfaces001/Amended the test suite to report updated documentation. 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 interfaces008/Add blank line after "large" messages interfaces009/Add CHANGELOG entry and test interfaces010/Add regression test for #2349 (#4584) interpret001/Interpreter tests (#3747) interpret002/Interpreter tests (#3747) interpret003/Add test for REPL reporting abnormal :exec results io001/Purify Idris of "return" io002/Purify Idris of "return" io003/prim__vm needs to take a World reference layout001/Use iWarn for parse errors literate001/Compose Docs meta001/Hide more features behind %language pragmas meta002/Don't include '=' for RHS span meta003/Add test from the pull request for Elab.tryCatch meta004/Add blank line after "large" messages pkg001/use HTTPS URL instead of HTTP URL when possible pkg002/make the tests respect the IDRIS env variable pkg003/make the tests respect the IDRIS env variable pkg004/Fix test for Windows path separators 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/Fix appveyor pkg009/[ fix ] handle empty NS + test case pkg010/Update test010. prelude001/make lines and unlines agree with Haskell primitives001/make the tests respect the IDRIS env variable primitives002/Set "--port none" in tests primitives003/add test cases verifying new verbatim string behavior primitives004-disabled/make the tests respect the IDRIS env variable primitives005/Bump test number. primitives006/Purify Idris of "return" proof001/Add blank line after "large" messages proof002/Fix binding rules in patterns proof003/Add blank line after "large" messages proof004/Fix formatting of some tests proof005/Fix formatting of some tests proof006/Fix formatting of some tests proof007/Don't include '=' for RHS span proof008/Add blank line after "large" messages proof009/Fix name decoration proof010/Change Instance to implementation (#3404) proof011/Don't include '=' for RHS span 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/Get rid of warnings in pruviloj test quasiquote001/Remove old eliminator generation and induction tactic (#4351) quasiquote002/make the tests respect the IDRIS env variable quasiquote003/Don't include '=' for RHS span quasiquote004/Don't include '=' for RHS span quasiquote005/make the tests respect the IDRIS env variable quasiquote006/Don't include '=' for RHS span 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/Add blank line after "large" messages 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/Add blank line after "large" messages 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/Change DecEq primitives to use believe_me regression002/Handle constant negation in parsing phase regression003/Merge branch 'master' of github.com:idris-lang/Idris-dev into add_regression_test_js_unexpected_con_as_glob scripts/Move `timeout` from `test/bin/` to `test/scripts/` sourceLocation001/Don't include '=' for RHS span st001/Updated comments according to review comments: st002/First attempt at implementing ST alternative for File.idr in Effects. st003/First attempt at implementing ST alternative for File.idr in Effects. st004/First attempt at implementing ST alternative for File.idr in Effects. st005/First attempt at implementing ST alternative for File.idr in Effects. st006/First attempt at implementing ST alternative for File.idr in Effects. st007/First attempt at implementing ST alternative for File.idr in Effects. sugar001/make the tests respect the IDRIS env variable sugar002/make the tests respect the IDRIS env variable sugar003/Purify Idris of "return" sugar004/Update the test for let- and bind-alternatives sugar005/Fix binding rules in patterns syntax001/Add blank line after "large" messages syntax002/make the tests respect the IDRIS env variable tactics001/Hide more features behind %language pragmas totality001/Add blank line after "large" messages totality002/Add blank line after "large" messages totality003/Add blank line after "large" messages totality004/Add blank line after "large" messages totality005/make the tests respect the IDRIS env variable totality006/Add blank line after "large" messages totality007/Add blank line after "large" messages totality008/Add blank line after "large" messages totality009/Don't include '=' for RHS span totality010/Add blank line after "large" messages totality011/Fix binding rules in patterns totality012/Add blank line after "large" messages totality013/Add blank line after "large" messages totality014/Don't include '=' for RHS span totality015/Add blank line after "large" messages totality016/Add blank line after "large" messages totality017/Add blank line after "large" messages totality018/Add blank line after "large" messages totality019/Add blank line after "large" messages totality020/Add blank line after "large" messages totality021/Add blank line after "large" messages totality022/Add blank line after "large" messages totality023/Add blank line after "large" messages totality024/Add test for totality checking of partially applied function totality025/Add tests for #4282 and #4299 totality026/Add tests for #4282 and #4299 tutorial001/Fix formatting of some tests tutorial002/Add blank line after "large" messages tutorial003/make the tests respect the IDRIS env variable tutorial004/Add blank line after "large" messages tutorial005/make the tests respect the IDRIS env variable tutorial006/Don't include '=' for RHS span tutorial007/Fix formatting of some tests unique001/Hide more features behind %language pragmas unique004/Don't include '=' for RHS span universes001/Don't include '=' for RHS span universes002/Don't include '=' for RHS span views001/fix broken tests caused by `mod` precedence views002/fix broken tests caused by `mod` precedence views003/Convention says the function should be 'vList' README.mdFirst attempt at implementing ST alternative for File.idr in Effects. TestData.hsfix Core.Execute and test TestRun.hsOnly check for Node when required mktest.plFix warning for implicitable names