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