diff --git a/tests/Main.idr b/tests/Main.idr index 3ed909153..38e8551ed 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -32,8 +32,8 @@ ttimpTests = MkTestPool [] "qtt001", "qtt003", "total001", "total002", "total003"] -idrisTests : TestPool -idrisTests = MkTestPool [] +idrisTestsBasic : TestPool +idrisTestsBasic = MkTestPool [] -- Fundamental language features ["basic001", "basic002", "basic003", "basic004", "basic005", "basic006", "basic007", "basic008", "basic009", "basic010", @@ -45,60 +45,91 @@ idrisTests = MkTestPool [] "basic036", "basic037", "basic038", "basic039", "basic040", "basic041", "basic042", "basic043", "basic044", "basic045", "basic046", "basic047", "basic048", "basic049", "basic050", - "basic051", + "basic051"] + +idrisTestsCoverage : TestPool +idrisTestsCoverage = MkTestPool [] -- Coverage checking - "coverage001", "coverage002", "coverage003", "coverage004", + ["coverage001", "coverage002", "coverage003", "coverage004", "coverage005", "coverage006", "coverage007", "coverage008", - "coverage009", "coverage010", "coverage011", - -- Documentation strings - "docs001", "docs002", - -- Evaluator - "evaluator001", "evaluator002", "evaluator003", "evaluator004", + "coverage009", "coverage010", "coverage011"] + +idrisTestsError : TestPool +idrisTestsError = MkTestPool [] -- Error messages - "error001", "error002", "error003", "error004", "error005", + ["error001", "error002", "error003", "error004", "error005", "error006", "error007", "error008", "error009", "error010", "error011", "error012", "error013", "error014", - -- Modules and imports - "import001", "import002", "import003", "import004", "import005", + -- Parse errors + "perror001", "perror002", "perror003", "perror004", "perror005", + "perror006"] + +idrisTestsInteractive : TestPool +idrisTestsInteractive = MkTestPool [] -- Interactive editing support - "interactive001", "interactive002", "interactive003", "interactive004", + ["interactive001", "interactive002", "interactive003", "interactive004", "interactive005", "interactive006", "interactive007", "interactive008", "interactive009", "interactive010", "interactive011", "interactive012", "interactive013", "interactive014", "interactive015", "interactive016", - "interactive017", "interactive018", "interactive019", + "interactive017", "interactive018", "interactive019"] + +idrisTestsInterface : TestPool +idrisTestsInterface = MkTestPool [] -- Interfaces - "interface001", "interface002", "interface003", "interface004", + ["interface001", "interface002", "interface003", "interface004", "interface005", "interface006", "interface007", "interface008", "interface009", "interface010", "interface011", "interface012", "interface013", "interface014", "interface015", "interface016", "interface017", "interface018", "interface019", "interface020", - "interface021", + "interface021"] + +idrisTestsLinear : TestPool +idrisTestsLinear = MkTestPool [] + -- QTT and linearity related + ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping + "linear005", "linear006", "linear007", "linear008", + "linear009", "linear010", "linear011", "linear012"] + +idrisTestsLiterate : TestPool +idrisTestsLiterate = MkTestPool [] + -- Literate + ["literate001", "literate002", "literate003", "literate004", + "literate005", "literate006", "literate007", "literate008", + "literate009", "literate010", "literate011", "literate012", + "literate013", "literate014", "literate015", "literate016"] + +idrisTestsPerformance : TestPool +idrisTestsPerformance = MkTestPool [] + -- Performance: things which have been slow in the past, or which + -- pose interesting challenges for the elaborator + ["perf001", "perf002", "perf003", "perf004", "perf005", "perf006"] + +idrisTestsRegression : TestPool +idrisTestsRegression = MkTestPool [] + -- Miscellaneous regressions + ["reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007", + "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", + "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021", + "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", + "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035"] + +idrisTests : TestPool +idrisTests = MkTestPool [] + -- Documentation strings + ["docs001", "docs002", + -- Evaluator + "evaluator001", "evaluator002", "evaluator003", "evaluator004", + -- Modules and imports + "import001", "import002", "import003", "import004", "import005", -- Miscellaneous REPL "interpreter001", "interpreter002", "interpreter003", "interpreter004", "interpreter005", "interpreter006", -- Implicit laziness, lazy evaluation "lazy001", - -- QTT and linearity related - "linear001", "linear002", "linear003", - -- "linear004" -- disabled due to requiring linearity subtyping - "linear005", - "linear006", "linear007", "linear008", "linear009", "linear010", - "linear011", "linear012", - -- Literate - "literate001", "literate002", "literate003", "literate004", - "literate005", "literate006", "literate007", "literate008", - "literate009", "literate010", "literate011", "literate012", - "literate013", "literate014", "literate015", "literate016", -- Namespace blocks "namespace001", -- Parameters blocks "params001", - -- Performance: things which have been slow in the past, or which - -- pose interesting challenges for the elaborator - "perf001", "perf002", "perf003", "perf004", "perf005", "perf006", - -- Parse errors - "perror001", "perror002", "perror003", "perror004", "perror005", - "perror006", -- Packages and ipkg files "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", -- Positivity checking @@ -113,12 +144,6 @@ idrisTests = MkTestPool [] "reflection001", "reflection002", "reflection003", "reflection004", "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", - -- Miscellaneous regressions - "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007", - "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", - "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021", - "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", - "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035", -- Totality checking "total001", "total002", "total003", "total004", "total005", "total006", "total007", "total008", "total009", "total010", @@ -151,9 +176,10 @@ racketTests = MkTestPool [Racket] nodeTests : TestPool nodeTests = MkTestPool [Node] - [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009" - , "node011", "node012", "node015", "node017", "node018", "node019" -- node014 - , "node021", "node022" --, "node020" + [ "node001", "node002", "node003", "node004", "node005", "node006" + , "node007", "node008", "node009", "node011", "node012", "node015" + , "node017", "node018", "node019", "node021", "node022" + -- , "node14", "node020" , "reg001" , "syntax001" , "tailrec001" @@ -175,6 +201,15 @@ templateTests = MkTestPool [] main : IO () main = runner [ testPaths "ttimp" ttimpTests + , testPaths "idris2" idrisTestsBasic + , testPaths "idris2" idrisTestsCoverage + , testPaths "idris2" idrisTestsError + , testPaths "idris2" idrisTestsInteractive + , testPaths "idris2" idrisTestsInterface + , testPaths "idris2" idrisTestsLiterate + , testPaths "idris2" idrisTestsLinear + , testPaths "idris2" idrisTestsPerformance + , testPaths "idris2" idrisTestsRegression , testPaths "idris2" idrisTests , testPaths "typedd-book" typeddTests , testPaths "ideMode" ideModeTests