@@ -4,18 +4,27 @@
4Testing Idris Packages
4Testing Idris Packages
5**********************
5**********************
7−As part of the integrated build system a simple testing framework is provided.
7+The integrated build system includes a simple testing framework.
8−This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.
8+This framework collects functions listed in the ``ipkg`` file under ``tests``.
9−This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.
9+All test functions must return ``IO ()``.
12−It is up to the developer to ensure the correct reporting of test results, and the structure and nature of how the tests are run.
12+When you enter ``idris --testpkg yourmodule.ipkg``,
13−Further, all test functions must return ``IO ()``, and must be listed in the ``ipkg`` file under ``tests``, and rhe modules containing the test functions must also be listed in the modules section of the ``iPKG`` file.
13+the build system creates a temporary file in a fresh environment on your machine
14+by listing the ``tests`` functions under a single ``main`` function.
15+It compiles this temporary file to an executable and then executes it.
18+The tests themselves are responsible for reporting their success or failure.
19+Test functions commonly use ``putStrLn`` to report test results.
20+The test framework does not impose any standards for reporting and consequently
21+does not aggregate test results.
16For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
24For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
18.. code-block:: idris
26.. code-block:: idris
27+ :caption: Math/NumOps.idr
20 module Maths.NumOps
29 module Maths.NumOps
@@ -28,6 +37,7 @@ For example, lets take the following list of functions that are defined in a mod
28A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
37A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
30.. code-block:: idris
39.. code-block:: idris
40+ :caption: Math/TestOps.idr
32 module Test.NumOps
42 module Test.NumOps
@@ -36,12 +46,12 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
36 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
46 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
37 assertEq g e = if g == e
47 assertEq g e = if g == e
38 then putStrLn "Test Passed"
48 then putStrLn "Test Passed"
39− else putStrLn "Test failed"
49+ else putStrLn "Test Failed"
41 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
51 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
42 assertNotEq g e = if not (g == e)
52 assertNotEq g e = if not (g == e)
43 then putStrLn "Test Passed"
53 then putStrLn "Test Passed"
44− else putStrLn "Test failed"
54+ else putStrLn "Test Failed"
46 testDouble : IO ()
56 testDouble : IO ()
47 testDouble = assertEq (double 2) 4
57 testDouble = assertEq (double 2) 4
@@ -53,13 +63,23 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
53The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
63The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
54The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
64The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
56− module maths
66+ package maths
58− module = Maths.NumOps
68+ modules = Maths.NumOps
59− , Test.NumOps
69+ , Test.NumOps
61 tests = Test.NumOps.testDouble
71 tests = Test.NumOps.testDouble
62 , Test.NumOps.testTriple
72 , Test.NumOps.testTriple
65−The testing framework can be invoked using: ``idris --testpkg maths.ipkg``.
75+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
77+ > idris --testpkg maths.ipkg
78+ Type checking ./Maths/NumOps.idr
79+ Type checking ./Test/NumOps.idr
80+ Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
84+Note how both tests have reported success by printing ``Test Passed``
85+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.