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
5c9ffda026
Idris-dev/test
History
Matus Tejiscak 5c9ffda026 Fix dependent pair names in reg030.
2014-05-28 15:57:36 +01:00
..
basic001 Fix reg005. 2014-04-11 09:08:27 +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 Add application context to all error messages 2014-03-22 10:01:11 +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
effects001 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
effects002 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
error001 Categorise tests 2014-01-30 17:24:08 +00:00
error002 Categorise tests 2014-01-30 17:24:08 +00:00
error003 Support mixed induction/coinduction with Inf type 2014-03-22 17:46:14 +00:00
error004 Coverage checker fix 2014-04-02 00:04:07 +01: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 Control whether provider decls accept postulates 2014-02-26 15:01:01 +01: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 Categorise tests 2014-01-30 17:24:08 +00:00
primitives003 Categorise tests 2014-01-30 17:24:08 +00:00
proof001 Categorise tests 2014-01-30 17:24:08 +00:00
proof002 Update for new unification error messages 2014-03-20 20:00:18 +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 Tests on default args and substitution 2014-04-06 01:22:27 +03: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 Added nested record access syntax 2014-05-02 08:58:57 +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 Implicit "module Main" added 2014-01-18 22:11:59 +00: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
reg008 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg009 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg010 Rewrite error printing to use the pretty-printer 2014-01-28 13:57:11 +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 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00: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 Merge pull request #1204 from david-christiansen/totality-warning 2014-05-08 17:17:15 +02: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 Update result of reg028 2013-11-30 13:53:23 +00:00
reg029 started working on new cmd arg parser 2014-05-14 18:39:47 +02:00
reg030 Fix dependent pair names in reg030. 2014-05-28 15:57:36 +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 Add application context to all error messages 2014-03-22 10:01:11 +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
reg043 Fix precedence of application vs arrows in pprint 2014-05-04 19:43:12 +02:00
reg044 Check that proof steps introduce no new problems 2014-05-22 12:14:51 +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 Add assert_smaller function 2014-02-01 22:52:22 +00: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
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 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
Makefile Replace records003 test 2014-05-04 13:27:53 +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