record Options : Type
Options for the test driver.
Totality: total
Visibility: public export
Constructor: MkOptions : String -> Maybe String -> Maybe (String -> Bool) -> Bool -> Bool -> Bool -> Nat -> Maybe String -> Options
Projections:
.codegen : Options -> Maybe String
Which codegen should we use?
.color : Options -> Bool
Should we use colors?
.exeUnderTest : Options -> String
Name of the idris2 executable
.failureFile : Options -> Maybe String
Should we write the list of failing cases to a file?
.interactive : Options -> Bool
Should we run the test suite interactively?
.onlyNames : Options -> Maybe (String -> Bool)
Should we only run some specific cases?
.threads : Options -> Nat
How many threads should we use?
.timing : Options -> Bool
Should we time and display the tests
.exeUnderTest : Options -> String
Name of the idris2 executable
Visibility: public exportexeUnderTest : Options -> String
Name of the idris2 executable
Visibility: public export.codegen : Options -> Maybe String
Which codegen should we use?
Visibility: public exportcodegen : Options -> Maybe String
Which codegen should we use?
Visibility: public export.onlyNames : Options -> Maybe (String -> Bool)
Should we only run some specific cases?
Visibility: public exportonlyNames : Options -> Maybe (String -> Bool)
Should we only run some specific cases?
Visibility: public export.interactive : Options -> Bool
Should we run the test suite interactively?
Visibility: public exportinteractive : Options -> Bool
Should we run the test suite interactively?
Visibility: public export.color : Options -> Bool
Should we use colors?
Visibility: public exportcolor : Options -> Bool
Should we use colors?
Visibility: public export.timing : Options -> Bool
Should we time and display the tests
Visibility: public exporttiming : Options -> Bool
Should we time and display the tests
Visibility: public export.threads : Options -> Nat
How many threads should we use?
Visibility: public exportthreads : Options -> Nat
How many threads should we use?
Visibility: public export.failureFile : Options -> Maybe String
Should we write the list of failing cases to a file?
Visibility: public exportfailureFile : Options -> Maybe String
Should we write the list of failing cases to a file?
Visibility: public exportinitOptions : String -> Bool -> Options
- Visibility: export
usage : String
- Visibility: export
options : List String -> IO (Maybe Options)
Process the command line options.
Visibility: exportrunTest : Options -> String -> IO Result
Run the specified Golden test with the supplied options.
See the module documentation for more information.
@testPath the directory that contains the test.
Visibility: exportpathLookup : List String -> IO (Maybe String)
Find the first occurrence of an executable on `PATH`.
Visibility: exportdata Requirement : Type
Some test may involve Idris' backends and have requirements.
We define here the ones supported by Idris
Totality: total
Visibility: public export
Constructors:
C : Requirement
Chez : Requirement
Node : Requirement
Racket : Requirement
Gambit : Requirement
Hints:
Eq Requirement
Eq Requirement
Show Requirement
Show Requirement
checkRequirement : Requirement -> IO (Maybe String)
- Visibility: export
findCG : IO (Maybe String)
- Visibility: export
data Codegen : Type
A choice of a codegen
Totality: total
Visibility: public export
Constructors:
Nothing : Codegen
Do NOT pass a cg argument to the executable being tested
Default : Codegen
Use whatever the test runner was passed at the toplevel,
and if nothing was passed guess a sensible default using findCG
Just : Requirement -> Codegen
Use exactly the given requirement
toList : Codegen -> List Requirement
- Visibility: export
record TestPool : Type
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
Totality: total
Visibility: public export
Constructor: MkTestPool : String -> List Requirement -> Codegen -> List String -> TestPool
Projections:
.codegen : TestPool -> Codegen
.constraints : TestPool -> List Requirement
.poolName : TestPool -> String
.testCases : TestPool -> List String
.poolName : TestPool -> String
- Visibility: public export
poolName : TestPool -> String
- Visibility: public export
.constraints : TestPool -> List Requirement
- Visibility: public export
constraints : TestPool -> List Requirement
- Visibility: public export
.codegen : TestPool -> Codegen
- Visibility: public export
codegen : TestPool -> Codegen
- Visibility: public export
.testCases : TestPool -> List String
- Visibility: public export
testCases : TestPool -> List String
- Visibility: public export
testsInDir : String -> {default (const True) _ : (String -> Bool)} -> String -> {default [] _ : List Requirement} -> {default Nothing _ : Codegen} -> IO TestPool
Find all the test in the given directory.
Visibility: exportfilterTests : Options -> List String -> List String
Only keep the tests that have been asked for
Visibility: exportrecord Summary : Type
The summary of a test pool run
Totality: total
Visibility: public export
Constructor: MkSummary : List String -> List String -> Summary
Projections:
.failure : Summary -> List String
.success : Summary -> List String
Hints:
Monoid Summary
Monoid Summary
Semigroup Summary
Semigroup Summary
.success : Summary -> List String
- Visibility: public export
success : Summary -> List String
- Visibility: public export
.failure : Summary -> List String
- Visibility: public export
failure : Summary -> List String
- Visibility: public export
initSummary : Summary
A new, blank summary
Visibility: exportupdateSummary : Result -> Summary -> Summary
Update the summary to contain the given result
Visibility: exportbulkUpdateSummary : List Result -> Summary -> Summary
Update the summary to contain the given results
Visibility: exportdata ThreadInstruction : Type
An instruction to a thread which runs tests
Totality: total
Visibility: public export
Constructors:
Run : String -> ThreadInstruction
A test to run
Stop : ThreadInstruction
An indication for the thread to stop
testSender : Channel ThreadInstruction -> Nat -> List String -> IO ()
Sends the given tests on the given @Channel@, then sends `nThreads` many
'Stop' @ThreadInstruction@s to stop the threads running the tests.
@testChan The channel to send the tests over.
@nThreads The number of threads being used to run the tests.
@tests The list of tests to send to the runners/threads.
Visibility: exportdata ThreadResult : Type
A result from a test-runner/thread
Totality: total
Visibility: public export
Constructors:
Res : Result -> ThreadResult
The result of running a test
Done : ThreadResult
An indication that the thread was told to stop
testReceiver : Channel ThreadResult -> Summary -> Channel Summary -> Nat -> IO ()
Receives results on the given @Channel@, accumulating them as a @Summary@.
When all results have been received (i.e. @nThreads@ many 'Done'
@ThreadInstruction@s have been encountered), send the resulting Summary over
the @accChan@ Channel (necessary to be able to @fork@ this function and
still obtain the Summary at the end).
@resChan The channel to receives the results on.
@acc The Summary acting as an accumulator.
@accChan The Channel to send the final Summary over.
@nThreads The number of threads being used to run the tests.
Visibility: exportpoolRunner : Options -> TestPool -> IO Summary
A runner for a test pool. If there are tests in the @TestPool@ that we want
to run, spawns `opts.threads` many runners and sends them the tests,
collecting all the results in the @Summary@ returned at the end.
@opts The options for the TestPool.
@pool The TestPool to run.
Visibility: exportrunnerWith : Options -> List TestPool -> IO ()
- Visibility: export
runner : List TestPool -> IO ()
A runner for a whole test suite
Visibility: export