@@ -4,18 +4,27 @@
44Testing Idris Packages
55**********************
66
7−As part of the integrated build system a simple testing framework is provided.
8−This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.
9−This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.
7+The integrated build system includes a simple testing framework.
8+This framework collects functions listed in the ``ipkg`` file under ``tests``.
9+All test functions must return ``IO ()``.
1010
1111
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.
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.
12+When you enter ``idris --testpkg yourmodule.ipkg``,
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.
16+
17+
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.
1422
1523
1624For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
1725
1826.. code-block:: idris
27+ :caption: Math/NumOps.idr
1928
2029 module Maths.NumOps
2130
@@ -28,6 +37,7 @@ For example, lets take the following list of functions that are defined in a mod
2837A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
2938
3039.. code-block:: idris
40+ :caption: Math/TestOps.idr
3141
3242 module Test.NumOps
3343
@@ -36,12 +46,12 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
3646 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
3747 assertEq g e = if g == e
3848 then putStrLn "Test Passed"
39− else putStrLn "Test failed"
49+ else putStrLn "Test Failed"
4050
4151 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
4252 assertNotEq g e = if not (g == e)
4353 then putStrLn "Test Passed"
44− else putStrLn "Test failed"
54+ else putStrLn "Test Failed"
4555
4656 testDouble : IO ()
4757 testDouble = assertEq (double 2) 4
@@ -53,13 +63,23 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
5363The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
5464The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
5565
56− module maths
66+ package maths
5767
58− module = Maths.NumOps
59− , Test.NumOps
68+ modules = Maths.NumOps
69+ , Test.NumOps
6070
6171 tests = Test.NumOps.testDouble
6272 , Test.NumOps.testTriple
6373
6474
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``::
76+
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
81+ Test Passed
82+ Test Passed
83+
84+Note how both tests have reported success by printing ``Test Passed``
85+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.