ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity
b591600d12
Idris-dev/test
History
Edwin Brady b591600d12 Don't propagate unique names to 'where' 
Doing so breaks typechecking, leading to nothing working any more...
passing them to lifted 'where' definitions counts as a use in the
typechecker, so *any* where clause will fail to typecheck.

This is an effect of how 'where' clauses are elaborated, and is probably
not the best behaviour (though it is better than the default which rules
our where clauses completely) so we should revisit it later if
uniqueness typing turns out to work effectively.
2014-08-26 09:25:10 +01:00
..
basic001 Better treatment of unbound implicits 2014-07-08 02:40:37 +01:00
basic002 Fix usage in basic002. 2014-04-11 09:10:25 +01:00
basic003 Categorise tests 2014-01-30 17:24:08 +00:00
basic004 Categorise tests 2014-01-30 17:24:08 +00:00
basic005 Categorise tests 2014-01-30 17:24:08 +00:00
basic006 Remove implicit qualifier for 'effect' 2014-05-25 17:05:27 +02:00
basic007 Return test033 to the original state. 2014-04-11 09:10:25 +01:00
basic008 Categorise tests 2014-01-30 17:24:08 +00:00
basic009 Keep type arguments of = when unelaborating 2014-07-09 21:15:06 +01:00
basic010 Add a timeout. 2014-05-29 13:55:04 +01:00
bounded001 Port Haskell's Bounded class 2014-02-21 14:47:24 +01:00
buffer001-disabled Temporarily disable buffer001 test 2014-02-01 20:36:51 +00:00
dsl001 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
dsl002 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
dsl003 Add pi to overridable syntax in DSL blocks 2014-06-09 23:39:00 +02:00
effects001 Replace 'effects' with neweffects 2014-07-15 21:35:35 +02:00
effects002 Replace 'effects' with neweffects 2014-07-15 21:35:35 +02:00
error001 Categorise tests 2014-01-30 17:24:08 +00:00
error002 Categorise tests 2014-01-30 17:24:08 +00:00
error003 Remove dodgy unification hack 2014-07-11 14:26:30 +01:00
error004 Make proof arguments to list functions implicit 2014-07-25 00:24:30 +02:00
ffi001 Avoid pollution of test case with ANSI codes 2014-02-04 13:27:57 +01:00
ffi002 Test updates for executor and type provider update 2014-02-03 11:07:11 +01:00
ffi003 Update test to avoid interactive-mode control chars 2014-02-04 13:50:45 +01:00
ffi004 Remove reliance on interactive output from test ffi004 2014-02-04 14:29:05 +01:00
ffi005 Distinguish postulate providers and type providers at use site 2014-06-05 13:53:03 +02:00
folding001 Tests for tail recursive implementations of foldr 2014-03-11 18:42:05 +01:00
folding002 Change type class top level method generation 2014-05-13 00:34:11 +01:00
idrisdoc001 Namespaces only containing private members is now correctly considered empty 2014-04-30 15:06:21 +02:00
idrisdoc002 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc003 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc004 Fixed typo 2014-04-25 01:52:07 +02:00
idrisdoc005 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc006 Updated idrisdoc006 to be more throughly 2014-04-30 16:37:45 +02:00
idrisdoc007 Made test resistant to differences among command implementations 2014-04-23 10:20:25 +02:00
idrisdoc008 Added IdrisDoc test which verifies inclusion of abstract and public namespace members 2014-04-30 17:08:42 +02:00
interactive001 Fix interactive editing and tests 2014-05-02 14:36:34 +02:00
interactive002 Improve inference in monadic code 2014-02-10 10:11:00 +00:00
interactive003 Fix interactive editing and tests 2014-05-02 14:36:34 +02:00
interactive004 Add :refine (:ref) command for refining a hole 2014-04-17 15:41:06 +01:00
io001 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
io002 Categorise tests 2014-01-30 17:24:08 +00:00
io003 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
literate001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives002 Truncate results in primitives002 test 2014-08-09 14:08:15 +01:00
primitives003 Categorise tests 2014-01-30 17:24:08 +00:00
proof001 Categorise tests 2014-01-30 17:24:08 +00:00
proof002 More efficiency improvements 2014-08-06 18:25:01 +01:00
proof003 Add --nowarnreach to two tests. 2014-04-11 09:10:26 +01:00
proof004 Categorise tests 2014-01-30 17:24:08 +00:00
proof005 'Reject' cases to default arg substitution tests. 2014-04-06 02:06:46 +03:00
proof006 'Reject' cases to default arg substitution tests. 2014-04-06 02:06:46 +03:00
proof007 Use a zipper-like proof state 2014-08-03 21:14:50 +01:00
quasiquote001 Fix universe errors, update tests 2014-08-22 20:31:11 +01:00
quasiquote002 Add goal types to quasiquotes. 2014-06-30 18:49:22 +02:00
quasiquote003 Update tests for rechecking of quasiquotes 2014-07-14 11:18:24 +02:00
quasiquote004 Add tactics "skip" and "fail" 2014-07-24 23:26:52 +02:00
records001 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
records002 Rename record002 test to the correct name! 2014-05-01 21:39:34 +02:00
records003 Generate better record projection types 2014-07-16 14:02:37 +02:00
reg001 Remove apply from reg001 since it's in the prelude! 2014-01-18 19:52:21 +00:00
reg002 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
reg003 Better treatment of unbound implicits 2014-07-08 02:40:37 +01:00
reg004 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg005 Categorise tests 2014-01-30 17:24:08 +00:00
reg006 Fix earlier %assert_total propagation 2014-01-03 01:31:01 +00:00
reg007 Support mixed induction/coinduction with Inf type 2014-03-22 17:46:14 +00:00
reg009 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg010 Inline with blocks 2014-08-19 16:21:00 +01:00
reg011 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg012 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg013 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg014 Add Prelude.Vect.transpose 2014-05-30 16:44:14 +02:00
reg015 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg016 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg017 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg018 Inline with blocks 2014-08-19 16:21:00 +01:00
reg019 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg020 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg021 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg022 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg023 Rewrite error printing to use the pretty-printer 2014-01-28 13:57:11 +01:00
reg024 Adjust tests to the changed String show instance 2013-11-25 18:10:46 +01:00
reg025 Fix usage in reg025. 2014-04-11 09:10:26 +01:00
reg026 Unification changes 2014-02-17 00:01:05 +00:00
reg027 Unification changes 2014-02-17 00:01:05 +00:00
reg028 Inline with blocks 2014-08-19 16:21:00 +01:00
reg029 fix missing tests 2014-06-07 22:01:16 +02:00
reg030 Fix reg030. 2014-05-29 15:44:00 +01:00
reg031 Make reg031 char-sign-indifferent. 2014-01-19 22:05:11 +00:00
reg032 Categorise tests 2014-01-30 17:24:08 +00:00
reg033 Fix silly name shadowing bug and add new test 2014-02-04 18:03:18 +00:00
reg034 Better treatment of unbound implicits 2014-07-08 02:40:37 +01:00
reg035 Evaluator bug fix 2014-02-21 17:57:11 +00:00
reg036 Fix parameter name propagation 2014-02-22 12:15:49 +00:00
reg037 Treat (=) as a special function name. 2014-03-05 12:46:23 +01:00
reg038 Tweak scoping rules in instance generation 2014-03-06 11:47:49 +00:00
reg039 Fix test reg039 and add it to idris.cabal 2014-04-15 13:26:39 +02:00
reg040 Rename test reg040 to avoid clash 2014-04-20 16:42:15 +01:00
reg041 Fix precedence of application vs arrows in pprint 2014-05-04 19:43:12 +02:00
reg042 Add a regression test. 2014-04-24 18:14:52 +01:00
reg044 Check that proof steps introduce no new problems 2014-05-22 12:14:51 +01:00
reg045 Deal with 'Delay' in case building properly 2014-06-09 20:48:03 +01:00
reg046 Remove dodgy unification hack 2014-07-11 14:26:30 +01:00
reg047 New regression test 2014-07-16 21:05:14 +02:00
reg048 Fixed bug regarding insertion in SortedMap. 2014-07-19 20:34:12 +02:00
reg049 Reinsert check for constructor/family mismatch. 2014-07-28 20:36:47 +02:00
reg050 Add regression test for operators starting with "!" 2014-07-30 00:47:17 +02:00
reg051 Store parameters in function types 2014-08-08 13:06:03 +01:00
sugar001 Categorise tests 2014-01-30 17:24:08 +00:00
sugar002 Categorise tests 2014-01-30 17:24:08 +00:00
sugar003 Categorise tests 2014-01-30 17:24:08 +00:00
sugar004 Syntax for failures in pattern matching let/<- 2014-03-07 20:57:43 +00:00
totality001 Don't try to compile a test that doesn't have main 2014-05-06 19:55:20 +02:00
totality002 Categorise tests 2014-01-30 17:24:08 +00:00
totality003 Fix a bug in qsort 2014-07-18 00:58:54 -07:00
totality004 Update test for totality warnings 2014-05-06 19:57:31 +02:00
totality005 Update for totality warnings 2014-05-06 19:50:32 +02:00
totality006 Tweak notion of recoverability in coverage checker 2014-04-20 21:51:34 +01:00
totality007 Stop building packages if there are totality mismatches 2014-05-09 20:48:41 +02:00
totality008 Find negative occurrences in positivity checker 2014-05-28 23:27:12 +02:00
tutorial001 Fix regression with data declarations in where 2014-03-10 20:47:41 +00:00
tutorial002 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial003 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial004 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial005 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial006 Inline with blocks 2014-08-19 16:21:00 +01:00
unique001 Really fix output of unique001a... 2014-08-22 21:09:16 +01:00
unique002 Don't propagate unique names to 'where' 2014-08-26 09:25:10 +01:00
unique003 Fix universe errors, update tests 2014-08-22 20:31:11 +01:00
Makefile Disable primitives003 test in LLVM back end 2014-08-20 12:03:09 +01:00
mktest.pl Change from shebangs with absolute references to using /usr/bin/env 2013-11-18 17:10:00 +00:00
README Added IdrisDoc tests 2014-04-22 23:44:15 +02:00
runtest.pl Add assert_smaller function 2014-02-01 22:52:22 +00:00

README 

Tests are categorised as follows:

basic:       Basic language features, some complete programs
dsl:         Embedded DSLs and features to support DSL development
effects:     Effects package
error:       Error messages and error reflection
ffi:         FFI calls, including type providers
idrisdoc:    Documentation tool functionality
interactive: Interactive editing, proof search
io:          IO monad
literate:    .lidr files; literate programming
primitives:  Primitive types
proof:       Theorem proving, tactics
sugar:       Syntactic sugar, syntax extensions
totality:    Totality checking
tutorial:    Examples from the tutorial

reg:         Regression tests, covering previous bug fixes