git.iko.soy/Idris-dev
on v1.3.1 help sign in
Idris-dev/test
255 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/Set "--port none" in tests docs002/Set "--port none" in tests docs003/Prelude: implement Functor for `Pair a` docs004/Set "--port none" in tests docs005/Set "--port none" in tests docs006/Print interface constraints as a separate section 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/Add blank line after "large" messages 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 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/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/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 interfaces008/Add blank line after "large" messages interfaces009/Add CHANGELOG entry and test 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/Introduce a PkgName abstraction to represent package name instead of String 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/Set stdout line buffering before building inputs pkg009/[ fix ] handle empty NS + test case pkg010/Fix package test 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 looped temporary allocations in mini-GMP (#4324) TestRun.hsUnused imports mktest.plFix warning for implicitable names