[ refactor ] to allow testpools to specify a backend (#1591)

.github/workflows/ci-macos-combined.yml

@@ -11,7 +11,6 @@ on:
 
 env:
   SCHEME: chez
-  IDRIS2_TESTS_CG: chez
 
 jobs:
 

.github/workflows/ci-ubuntu-combined.yml

@@ -25,7 +25,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: chez
-      IDRIS2_TESTS_CG: chez
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -47,7 +46,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: racket
-      IDRIS2_TESTS_CG: racket
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -67,7 +65,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: chez
-      IDRIS2_TESTS_CG: chez
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -111,7 +108,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: chez
-      IDRIS2_TESTS_CG: chez
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -137,7 +133,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: racket
-      IDRIS2_TESTS_CG: racket
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -161,7 +156,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: chez
-      IDRIS2_TESTS_CG: chez
     steps:
       - name: Checkout
         uses: actions/checkout@v2
@@ -194,7 +188,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       IDRIS2_CG: chez
-      IDRIS2_TESTS_CG: chez
     steps:
       - name: Checkout
         uses: actions/checkout@v2

.github/workflows/ci-windows.yml

@@ -12,7 +12,6 @@ env:
   MSYSTEM: MINGW64
   MSYS2_PATH_TYPE: inherit
   SCHEME: scheme
-  IDRIS2_TESTS_CG: chez
   CC: gcc
 
 jobs:

libs/test/README.md

@@ -1,14 +1,25 @@
 # Test
-The test package exposes the same test framework(s) the Idris 2 compiler uses for its test suite.
+The test package exposes the same test framework(s) the Idris 2 compiler
+uses for its test suite.
 
-In a language like Idris 2, there are a number of strategies one can take for testing their code and the eventual goal of this testing package is to facilitate a blend of these strategies in any project. Currently the package contains one module facilitating one style of testing: `Golden`. Contributions containing other modules that enable additional testing styles are encouraged.
+In a language like Idris 2, there are a number of strategies one can take
+for testing their code and the eventual goal of this testing package is to
+facilitate a blend of these strategies in any project. Currently the package
+contains one module facilitating one style of testing: `Golden`. Contributions
+containing other modules that enable additional testing styles are encouraged.
 
-To use the test package, either pass `-p test` to the idris2 executable or add `depends = test` to your test suite's package file.
+To use the test package, either pass `-p test` to the idris2 executable or
+add `depends = test` to your test suite's package file.
 
 ## Golden
-Golden facilitates testing by way of comparing test output with a predetermined expecation. The module is well documented in its own source code but the following is a primer.
 
-You first import the `Test.Golden` module and write an `IO` function to serve as the entrypoint for your test suite. This function must at some point call into Golden's `runner`.
+Golden facilitates testing by way of comparing a test's output to a
+predetermined expecation. The module is well documented in its own source code
+but the following is a primer.
+
+You first import the `Test.Golden` module and write an `IO` function to serve as
+the entrypoint for your test suite. This function must at some point call into
+Golden's `runner`.
 ```idris
 -- your_project/tests/Main.idr
 
@@ -23,10 +34,11 @@ main = do
   runner [tests]
 ```
 
-You populate the `TestPool` list that the `runner` expects with one entry per pool of tests you want to run. Within each pool, tests are run concurrently.
+You populate the `TestPool` list that the `runner` expects with one entry per
+pool of tests you want to run. Within each pool, tests are run concurrently.
 ```idris
 tests : TestPool
-tests = MkTestPool "Description of the test pool" [] [
+tests = MkTestPool "Description of the test pool" [] Nothing [
   "my_great_test"
 ]
 ```
@@ -34,9 +46,20 @@ tests = MkTestPool "Description of the test pool" [] [
 The first argument to `MkTestPool` is a description of the whole test pool.
 It will be printed before the tests from this pool are started.
 
-The second argument to `MkTestPool` (empty in the above example) is a list of codegen backends required to run the tests in the given pool. Any empty list means no requirements. If your tests required the Racket backend, you could instead specify `[Racket]`. See the [`Requirement` type](./Test/Golden.idr#L228) for more.
+The second argument to `MkTestPool` (empty in the above example) is a list of
+constraints that need to be satisfied to be able to run the tests in the given
+pool. An empty list means no requirements. If your tests required racket to be
+installed, you could for instance specify `[Racket]`.
+See the [`Requirement` type](./Test/Golden.idr#L228) for more.
 
-The third argument to `MkTestPool` is a list of directory names that can be found relative to your `Main.idr` file. This directory will have some combination of the following files.
+The third argument to `MkTestPool` is an optional backend. In the example we
+did not specify any but if you want to use the reference counting C backend
+you could for instance use `Just C`.
+
+
+The last argument is a list of directory names that can be found relative to
+your `Main.idr` file. This directory will have some combination of the following
+files.
 ```Shell
 my_great_test/
   Test.idr
@@ -47,16 +70,27 @@ my_great_test/
 ```
 
 These files define:
-1. Any Idris 2 source code needed for the test (Test.idr, which can be named anything you'd like and is not limited to 1 file).
+1. Any Idris 2 source code needed for the test
+  (Test.idr, which can be named anything you'd like and is not limited to 1 file).
 2. Any package information needed to build those source files (test.ipkg).
-3. The command run at the shell to execute your test (run).
+3. The command run at the shell to execute your test (run, use `$1` in place of the name of the idris2 executable).
 4. Optional input passed to your test case (input).
 5. The expected output of running your test (expected).
 
-See the [documentation](./Test/Golden.idr#L12) in `Test/Golden.idr` and the [template directories](../../tests/templates) provided with the Idris 2 project for a great primer on these files.
+See the [documentation](./Test/Golden.idr#L12) in `Test/Golden.idr` and
+the [template directories](../../tests/templates) provided with the Idris 2
+project for a great primer on these files.
 
-When you run your tests (the executable produced by building your `tests/Main.idr` file), you need to specify the Idris executable to use and optionally use interactive mode (`--interactive`) or limit the test cases that are run (`--only [names]`).
+When you run your tests (the executable produced by building your
-
+`tests/Main.idr` file), you need to specify the Idris executable to use
-Interactive mode is useful when you know the expected output for a test case is going to change -- you will be prompted to updated the expectation so you can choose whether the output produced by a new test run should become the new "golden" standard.
+and optionally set the interactive mode (`--interactive`), specify the
-You can even skip the step of creating an `expected` file altogether when you write a new test case and use interactive mode to accept the output of your test case as the expectation.
+number of threads to use concurrently (`--threads`), or limit the test
+cases that are run (`--only [names]`).
 
+Interactive mode is useful when you know the expected output for a test case
+is going to change -- you will be prompted to updated the expectation so you
+can choose whether the output produced by a new test run should become the new
+"golden" standard.
+You can even skip the step of creating an `expected` file altogether when you
+write a new test case and use interactive mode to accept the output of your
+test case as the expectation.

libs/test/Test/Golden.idr

@@ -205,11 +205,10 @@ export
 runTest : Options -> (testPath : String) -> IO (Future Result)
 runTest opts testPath = forkIO $ do
   start <- clockTime UTC
-  let cg = case codegen opts of
+  let cg = maybe "" (" --cg " ++) (codegen opts)
-         Nothing => ""
+  let exe = "\"" ++ exeUnderTest opts ++ cg ++ "\""
-         Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " "
   ignore $ system $ "cd " ++ testPath ++ " && " ++
-    cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output"
+    "sh ./run " ++ exe ++ " | tr -d '\\r' > output"
   end <- clockTime UTC
 
   Right out <- readFile $ testPath ++ "/output"
@@ -309,6 +308,14 @@ Show Requirement where
   show Racket = "racket"
   show Gambit = "gambit"
 
+export
+[CG] Show Requirement where
+  show C = "refc"
+  show Chez = "chez"
+  show Node = "node"
+  show Racket = "racket"
+  show Gambit = "gambit"
+
 export
 checkRequirement : Requirement -> IO (Maybe String)
 checkRequirement req
@@ -320,7 +327,7 @@ checkRequirement req
   where
     requirement : Requirement -> (String, List String)
     requirement C = ("CC", ["cc"])
-    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme"])
+    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "chezscheme", "scheme"])
     requirement Node = ("NODE", ["node"])
     requirement Racket = ("RACKET", ["racket"])
     requirement Gambit = ("GAMBIT", ["gsc"])
@@ -343,12 +350,14 @@ findCG
 ||| A test pool is characterised by
 |||  + a name
 |||  + a list of requirement
+|||  + a choice of codegen (overriding the default)
 |||  + and a list of directory paths
 public export
 record TestPool where
   constructor MkTestPool
   poolName : String
   constraints : List Requirement
+  codegen : Maybe Requirement
   testCases : List String
 
 ||| Only keep the tests that have been asked for
@@ -395,7 +404,7 @@ poolRunner opts pool
        let (_ :: _) = tests
              | [] => pure initSummary
        -- if so make sure the constraints are satisfied
-       cs <- for (constraints pool) $ \ req => do
+       cs <- for (toList (codegen pool) ++ constraints pool) $ \ req => do
           mfp <- checkRequirement req
           let msg = case mfp of
                       Nothing => "✗ " ++ show req ++ " not found"
@@ -407,8 +416,13 @@ poolRunner opts pool
 
        let Just _ = the (Maybe (List String)) (sequence cs)
              | Nothing => pure initSummary
+
+       -- if the test pool requires a specific codegen then use that
+       let opts = case codegen pool of
+                    Nothing => opts
+                    Just cg => { codegen := Just (show @{CG} cg) } opts
        -- if so run them all!
-       loop initSummary tests
+       loop opts initSummary tests
 
   where
 
@@ -421,12 +435,12 @@ poolRunner opts pool
        ++ msgs
        ++ [ separator, "" ]
 
-    loop : Summary -> List String -> IO Summary
+    loop : Options -> Summary -> List String -> IO Summary
-    loop acc [] = pure acc
+    loop opts acc [] = pure acc
-    loop acc tests
+    loop opts acc tests
       = do let (now, later) = splitAt opts.threads tests
            bs <- map await <$> traverse (runTest opts) now
-           loop (updateSummary bs acc) later
+           loop opts (updateSummary bs acc) later
 
 
 ||| A runner for a whole test suite
@@ -465,5 +479,3 @@ runner tests
          if nfail == 0
            then exitWith ExitSuccess
            else exitWith (ExitFailure 1)
-
--- [ EOF ]

tests/Main.idr

@@ -8,7 +8,7 @@ import Test.Golden
 -- Test cases
 
 ttimpTests : TestPool
-ttimpTests = MkTestPool "TTImp" []
+ttimpTests = MkTestPool "TTImp" [] Nothing
      [ "basic001", "basic002", "basic003", "basic004", "basic005"
      , "basic006"
      , "coverage001", "coverage002"
@@ -23,7 +23,7 @@ ttimpTests = MkTestPool "TTImp" []
      ]
 
 idrisTestsBasic : TestPool
-idrisTestsBasic = MkTestPool "Fundamental language features" []
+idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
       -- Fundamental language features
       ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006", "basic007", "basic008", "basic009", "basic010",
@@ -34,13 +34,13 @@ idrisTestsBasic = MkTestPool "Fundamental language features" []
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
-       "basic046", "basic047", "basic048", "basic049", "basic050",
+       "basic046", "basic047",             "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
        "basic061"]
 
 idrisTestsCoverage : TestPool
-idrisTestsCoverage = MkTestPool "Coverage checking" []
+idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
        -- Coverage checking
       ["coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
@@ -49,16 +49,16 @@ idrisTestsCoverage = MkTestPool "Coverage checking" []
        "coverage017"]
 
 idrisTestsCasetree : TestPool
-idrisTestsCasetree = MkTestPool "Case tree building" []
+idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
        -- Case tree building
       ["casetree001"]
 
 idrisTestsWarning : TestPool
-idrisTestsWarning = MkTestPool "Warnings" []
+idrisTestsWarning = MkTestPool "Warnings" [] Nothing
      ["warning001"]
 
 idrisTestsError : TestPool
-idrisTestsError = MkTestPool "Error messages" []
+idrisTestsError = MkTestPool "Error messages" [] Nothing
        -- Error messages
       ["error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
@@ -69,7 +69,7 @@ idrisTestsError = MkTestPool "Error messages" []
        "perror006", "perror007", "perror008"]
 
 idrisTestsInteractive : TestPool
-idrisTestsInteractive = MkTestPool "Interactive editing" []
+idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        -- Interactive editing support
       ["interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
@@ -82,7 +82,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" []
        "interactive033"]
 
 idrisTestsInterface : TestPool
-idrisTestsInterface = MkTestPool "Interface" []
+idrisTestsInterface = MkTestPool "Interface" [] Nothing
        -- Interfaces
       ["interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
@@ -93,7 +93,7 @@ idrisTestsInterface = MkTestPool "Interface" []
        "interface025"]
 
 idrisTestsLinear : TestPool
-idrisTestsLinear = MkTestPool "Quantities" []
+idrisTestsLinear = MkTestPool "Quantities" [] Nothing
        -- QTT and linearity related
        ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping
         "linear005", "linear006", "linear007", "linear008",
@@ -101,7 +101,7 @@ idrisTestsLinear = MkTestPool "Quantities" []
         "linear013", "linear014"]
 
 idrisTestsLiterate : TestPool
-idrisTestsLiterate = MkTestPool "Literate programming" []
+idrisTestsLiterate = MkTestPool "Literate programming" [] Nothing
        -- Literate
       ["literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
@@ -109,14 +109,14 @@ idrisTestsLiterate = MkTestPool "Literate programming" []
        "literate013", "literate014", "literate015", "literate016"]
 
 idrisTestsPerformance : TestPool
-idrisTestsPerformance = MkTestPool "Performance" []
+idrisTestsPerformance = MkTestPool "Performance" [] Nothing
        -- Performance: things which have been slow in the past, or which
        -- pose interesting challenges for the elaborator
-      ["perf001", "perf002", "perf003", "perf004", "perf005", "perf006",
+      ["perf001", "perf002", "perf003", "perf004", "perf005",
        "perf007", "perf008"]
 
 idrisTestsRegression : TestPool
-idrisTestsRegression = MkTestPool "Various regressions" []
+idrisTestsRegression = MkTestPool "Various regressions" [] Nothing
        -- Miscellaneous regressions
       ["reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
@@ -126,7 +126,7 @@ idrisTestsRegression = MkTestPool "Various regressions" []
        "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042"]
 
 idrisTestsData : TestPool
-idrisTestsData = MkTestPool "Data and record types" []
+idrisTestsData = MkTestPool "Data and record types" [] Nothing
       [-- Data types
        "data001",
        -- Records, access and dependent update
@@ -134,25 +134,34 @@ idrisTestsData = MkTestPool "Data and record types" []
        "record006", "record007", "record008"]
 
 idrisTestsBuiltin : TestPool
-idrisTestsBuiltin = MkTestPool "Builtin types and functions" []
+idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing
       -- %builtin related tests for the frontend (type-checking)
       ["builtin001", "builtin002", "builtin003", "builtin004", "builtin005",
        "builtin006", "builtin007", "builtin008", "builtin009", "builtin010",
        "builtin011"]
 
 idrisTestsEvaluator : TestPool
-idrisTestsEvaluator = MkTestPool "Evaluation" []
+idrisTestsEvaluator = MkTestPool "Evaluation" [] Nothing
       [ -- Evaluator
-       "evaluator001", "evaluator002", "evaluator003", "evaluator004",
+       "evaluator001", "evaluator002", "evaluator003",
-       -- Unfortunately the behaviour of Double is platform dependent so the
-       -- following test is turned off.
-       -- "evaluator005",
        -- Miscellaneous REPL
        "interpreter001", "interpreter002", "interpreter003", "interpreter004",
        "interpreter005", "interpreter006", "interpreter007"]
 
+idrisTestsAllBackends : Requirement -> TestPool
+idrisTestsAllBackends cg = MkTestPool
+      ("Test across all backends: " ++ show cg ++ " instance")
+      [] (Just cg)
+      [ -- Evaluator
+       "evaluator004",
+       -- Unfortunately the behaviour of Double is platform dependent so the
+       -- following test is turned off.
+       -- "evaluator005",
+       "basic048",
+       "perf006"]
+
 idrisTests : TestPool
-idrisTests = MkTestPool "Misc" []
+idrisTests = MkTestPool "Misc" [] Nothing
        -- Documentation strings
       ["docs001", "docs002", "docs003",
        -- Eta equality
@@ -188,14 +197,14 @@ idrisTests = MkTestPool "Misc" []
        "pretty001"]
 
 typeddTests : TestPool
-typeddTests = MkTestPool "Type Driven Development" []
+typeddTests = MkTestPool "Type Driven Development" [] Nothing
      [ "chapter01", "chapter02", "chapter03", "chapter04", "chapter05"
      , "chapter06", "chapter07", "chapter08", "chapter09", "chapter10"
      , "chapter11", "chapter12", "chapter13", "chapter14"
      ]
 
 chezTests : TestPool
-chezTests = MkTestPool "Chez backend" [Chez]
+chezTests = MkTestPool "Chez backend" [] (Just Chez)
     [ "chez001", "chez002", "chez003", "chez004", "chez005", "chez006"
     , "chez007", "chez008", "chez009", "chez010", "chez011", "chez012"
     , "chez013", "chez014", "chez015", "chez016", "chez017", "chez018"
@@ -214,14 +223,14 @@ chezTests = MkTestPool "Chez backend" [Chez]
     ]
 
 refcTests : TestPool
-refcTests = MkTestPool "Reference counting C backend" [C]
+refcTests = MkTestPool "Reference counting C backend" [] (Just C)
     [ "refc001" , "refc002"
     , "strings", "integers", "doubles"
     , "buffer", "clock", "args"
     ]
 
 racketTests : TestPool
-racketTests = MkTestPool "Racket backend" [Racket]
+racketTests = MkTestPool "Racket backend" [] (Just Racket)
     [ "forkjoin001"
     , "semaphores001", "semaphores002"
     , "futures001"
@@ -236,7 +245,7 @@ racketTests = MkTestPool "Racket backend" [Racket]
     ]
 
 nodeTests : TestPool
-nodeTests = MkTestPool "Node backend" [Node]
+nodeTests = MkTestPool "Node backend" [] (Just Node)
     [ "node001", "node002", "node003", "node004", "node005", "node006"
     , "node007", "node008", "node009", "node011", "node012", "node015"
     , "node017", "node018", "node019", "node021", "node022", "node023"
@@ -255,17 +264,17 @@ nodeTests = MkTestPool "Node backend" [Node]
     ]
 
 ideModeTests : TestPool
-ideModeTests = MkTestPool "IDE mode" []
+ideModeTests = MkTestPool "IDE mode" [] Nothing
   [ "ideMode001", "ideMode002", "ideMode003", "ideMode004", "ideMode005"
   ]
 
 preludeTests : TestPool
-preludeTests = MkTestPool "Prelude library" []
+preludeTests = MkTestPool "Prelude library" [] Nothing
   [ "reg001"
   ]
 
 templateTests : TestPool
-templateTests = MkTestPool "Test templates" []
+templateTests = MkTestPool "Test templates" [] Nothing
   [ "simple-test", "ttimp", "with-ipkg"
   ]
 
@@ -275,7 +284,7 @@ templateTests = MkTestPool "Test templates" []
 -- that only runs if all backends are
 -- available.
 baseLibraryTests : TestPool
-baseLibraryTests = MkTestPool "Base library" [Chez, Node]
+baseLibraryTests = MkTestPool "Base library" [Chez, Node] Nothing
   [ "system_file001"
   , "data_bits001"
   , "system_info001"
@@ -284,18 +293,18 @@ baseLibraryTests = MkTestPool "Base library" [Chez, Node]
 
 -- same behavior as `baseLibraryTests`
 contribLibraryTests : TestPool
-contribLibraryTests = MkTestPool "Contrib library" [Chez, Node]
+contribLibraryTests = MkTestPool "Contrib library" [Chez, Node] Nothing
   [ "json_001"
   ]
 
 codegenTests : TestPool
-codegenTests = MkTestPool "Code generation" []
+codegenTests = MkTestPool "Code generation" [] Nothing
   [ "con001"
   , "builtin001"
   ]
 
 main : IO ()
-main = runner
+main = runner $
   [ testPaths "ttimp" ttimpTests
   , testPaths "idris2" idrisTestsBasic
   , testPaths "idris2" idrisTestsCoverage
@@ -323,7 +332,11 @@ main = runner
   , testPaths "node" nodeTests
   , testPaths "templates" templateTests
   , testPaths "codegen" codegenTests
-  ] where
+  ]
+  ++ map (testPaths "allbackends" . idrisTestsAllBackends) [Chez, Node, Racket]
+
+
+    where
 
     testPaths : String -> TestPool -> TestPool
     testPaths dir = record { testCases $= map ((dir ++ "/") ++) }

tests/allbackends/basic048/run

@@ -1,5 +1,5 @@
 $1 --no-banner --no-color --console-width 0 "Module'.idr" < input
-$1 --exec main --cg ${IDRIS2_TESTS_CG} "Module'.idr"
+$1 --exec main "Module'.idr"
 EDITOR=true $1 --no-banner --no-color --console-width 0 "Module'.idr" < input-ed
 
 rm -rf build

tests/allbackends/evaluator004/run

@@ -1,4 +1,4 @@
 $1 --no-banner --no-color --console-width 0 Issue735.idr < input
-$1 --exec main --cg ${IDRIS2_TESTS_CG} Issue735.idr
+$1 --exec main Issue735.idr
 
 rm -rf build

tests/allbackends/evaluator005/run

@@ -0,0 +1,3 @@
+$1 --exec main Issue1200.idr
+
+rm -rf build

tests/allbackends/perf006/run

@@ -0,0 +1,3 @@
+$1 --exec main Issue775.idr
+
+rm -rf build

tests/chez/chez016/run

@@ -1,12 +1,4 @@
-# This test needs to run `idris2` from a sub-folder. Get the absolute path.
-
-if [ "$(uname)" = Darwin ]; then
-    IDRIS2_EXEC=$(zsh -c 'printf %s "$0:A"' "$1")
-else
-    IDRIS2_EXEC="$(readlink -f -- "$1")"
-fi
-
 cd "folder with spaces" || exit
 
-"$IDRIS2_EXEC" --no-color --console-width 0 --no-banner Main.idr < ../input
+$1 --no-color --console-width 0 --no-banner Main.idr < ../input
 rm -rf build

tests/idris2/builtin009/run

@@ -1,5 +1,3 @@
-$1 --no-color --console-width 0 --no-banner Test.idr -o test
+$1 --no-color --console-width 0 --no-banner --exec main Test.idr
-
-./build/exec/test
 
 rm -rf build

tests/idris2/builtin011/run

@@ -1,5 +1,3 @@
-$1 --no-color --console-width 0 --no-banner Test.idr -o test
+$1 --no-color --console-width 0 --no-banner --exec main Test.idr
-
-./build/exec/test
 
 rm -rf build

tests/idris2/evaluator005/run

@@ -1,3 +0,0 @@
-$1 --exec main --cg ${IDRIS2_TESTS_CG} Issue1200.idr
-
-rm -rf build

tests/idris2/perf006/run

@@ -1,3 +0,0 @@
-$1 --exec main --cg ${IDRIS2_TESTS_CG} Issue775.idr
-
-rm -rf build