Idris2Doc : Test.Golden


Core features required to perform Golden file testing.

We provide the core functionality to run a *single* golden file test, or
a whole test tree.
This allows the developer freedom to use as is or design the rest of the
test harness to their liking.

This was originally used as part of Idris2's own test suite and
the core functionality is useful for the many and not the few.
Please see Idris2 test harness for example usage.

# Test Structure

This harness works from the assumption that each individual golden test
comprises of a directory with the following structure:

+ `run` a *shell* script that runs the test. We expect it to:
  * Use `$1` as the variable standing for the idris executable to be tested
  * May use `${IDRIS2_TESTS_CG}` to pick a codegen that ought to work
  * Clean up after itself (e.g. by running `rm -rf build/`)

+ `expected` a file containting the expected output of `run`

During testing, the test harness will generate an artefact named `output`
and display both outputs if there is a failure.
During an interactive session the following command is used to compare them
as they are:

 git diff --no-index --exit-code --word-diff=color expected output

If `git` fails then the runner will simply present the expected and 'given'
files side-by-side.

Of note, it is helpful to add `output` to a local `.gitignore` instance
to ensure that it is not mistakenly versioned.

# Options

The test harness has several options that may be set:

+ `idris2`       The path of the executable we are testing.
+ `codegen`      The backend to use for code generation.
+ `onlyNames`    The tests to run relative to the generated executable.
+ `onlyFile`     The file listing the tests to run relative to the generated executable.
+ `interactive`  Whether to offer to update the expected file or not.
+ `timing`       Whether to display time taken for each test.
+ `threads`      The maximum numbers to use (default: number of cores).
+ `failureFile`  The file in which to write the list of failing tests.

We provide an options parser (`options`) that takes the list of command line
arguments and constructs this for you.

# Usage

When compiled to an executable the expected usage is:

runtests <path to executable under test>
  [--only-file PATH]
  [--failure-file PATH]
  [--threads N]
  [--cg CODEGEN]
  [--only [NAMES]]

assuming that the test runner is compiled to an executable named `runtests`.
dataCodegen : Type
  A choice of a codegen

Totality: total
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
recordOptions : Type
  Options for the test driver.

Totality: total
MkOptions : String -> MaybeString -> ListString -> Bool -> Bool -> Bool -> Nat -> MaybeString -> Options

.codegen : Options -> MaybeString
  Which codegen should we use?
.color : Options -> Bool
  Should we use colors?
.exeUnderTest : Options -> String
  Name of the idris2 executable
.failureFile : Options -> MaybeString
  Should we write the list of failing cases to a file?
.interactive : Options -> Bool
  Should we run the test suite interactively?
.onlyNames : Options -> ListString
  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
dataRequirement : Type
  Some test may involve Idris' backends and have requirements.
We define here the ones supported by Idris

Totality: total
C : Requirement
Chez : Requirement
Node : Requirement
Racket : Requirement
Gambit : Requirement
recordSummary : Type
  The summary of a test pool run

Totality: total
MkSummary : ListString -> ListString -> Summary

.failure : Summary -> ListString
.success : Summary -> ListString
recordTestPool : 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
MkTestPool : String -> ListRequirement -> Codegen -> ListString -> TestPool

.codegen : TestPool -> Codegen
.constraints : TestPool -> ListRequirement
.poolName : TestPool -> String
.testCases : TestPool -> ListString
checkRequirement : Requirement -> IO (MaybeString)
fail : String -> IOa
filterTests : Options -> ListString -> ListString
  Only keep the tests that have been asked for

findCG : IO (MaybeString)
initOptions : String -> Bool -> Options
initSummary : Summary
options : ListString -> IO (MaybeOptions)
  Process the command line options.

pathLookup : ListString -> IO (MaybeString)
  Find the first occurrence of an executable on `PATH`.

poolRunner : Options -> TestPool -> IOSummary
  A runner for a test pool

runTest : Options -> String -> IO (FutureResult)
  Run the specified Golden test with the supplied options.
See the module documentation for more information.
@testPath the directory that contains the test.

runner : ListTestPool -> IO ()
  A runner for a whole test suite

testsInDir : String -> (String -> Bool) -> String -> ListRequirement -> Codegen -> IOTestPool
  Find all the test in the given directory.

toList : Codegen -> ListRequirement
updateSummary : ListResult -> Summary -> Summary
usage : String