Test Refactor

.github/linters/.chktexrc

@@ -0,0 +1,14 @@
+########################
+########################
+## LaTeX Linter rules ##
+########################
+########################
+
+CmdLine {
+    # Command terminated with space.
+    --nowarn 1
+
+    # You ought to remove spaces in front of punctuation.
+    # This gets confused in code blocks, failing on eg. `x : Nat`
+    --nowarn 26
+}

.github/linters/.markdown-lint.yml

@@ -32,6 +32,7 @@ MD026:
 MD029: false                  # Ordered list item prefix
 MD033: false                  # Allow inline HTML
 MD036: false                  # Emphasis used instead of a heading
+MD041: false                  # First line in file should be a top level heading
 MD044:                        # Proper names should have the correct capitalization
   code_blocks: false
   html_elements: false

.github/workflows/ci-idris2.yml

@@ -483,7 +483,7 @@ jobs:
         run: make install-api
         shell: bash
       - name: Test API
-        run: cd tests/idris2/api001 && ./run idris2
+        run: cd tests/idris2/api/api001 && ./run "$HOME/.idris2/bin/idris2"
         shell: bash
 
   ######################################################################

libs/test/Test/Golden.idr

@@ -421,15 +421,21 @@ record TestPool where
 
 ||| Find all the test in the given directory.
 export
-testsInDir : (dirName : String) -> (testNameFilter : String -> Bool) -> (poolName : String) -> List Requirement -> Codegen -> IO TestPool
-testsInDir dirName testNameFilter poolName reqs cg = do
+testsInDir :
+  (dirName : String) ->
+  {default (const True) pred : String -> Bool} ->
+  (poolName : String) ->
+  {default [] requirements : List Requirement} ->
+  {default Nothing codegen : Codegen} ->
+  IO TestPool
+testsInDir dirName poolName = do
   Right names <- listDir dirName
     | Left e => die $ "failed to list " ++ dirName ++ ": " ++ show e
-  let names = [n | n <- names, testNameFilter n]
+  let names = [n | n <- names, pred n]
   let testNames = [dirName ++ "/" ++ n | n <- names]
   testNames <- filter testNames
   when (length testNames == 0) $ die $ "no tests found in " ++ dirName
-  pure $ MkTestPool poolName reqs cg testNames
+  pure $ MkTestPool poolName requirements codegen testNames
     where
       -- Directory without `run` file is not a test
       isTest : (path : String) -> IO Bool