testing.rst

.. _tut-sect-testing:

**********************
Testing Idris Packages
**********************

The integrated build system includes a simple testing framework.
This framework collects functions listed in the ``ipkg`` file under ``tests``.
All test functions must return ``IO ()``.


When you enter ``idris --testpkg yourmodule.ipkg``,
the build system creates a temporary file in a fresh environment on your machine
by listing the ``tests`` functions under a single ``main`` function.
It compiles this temporary file to an executable and then executes it.


The tests themselves are responsible for reporting their success or failure.
Test functions commonly use ``putStrLn`` to report test results.
The test framework does not impose any standards for reporting and consequently
does not aggregate test results.


For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

.. name: Math/NumOps.idr
.. code-block:: idris

    module Maths.NumOps

    double : Num a => a -> a
    double a = a + a

    triple : Num a => a -> a
    triple a = a + double a

A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

.. name: Math/TestOps.idr
.. code-block:: idris

    module Test.NumOps

    import Maths.NumOps

    assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
    assertEq g e = if g == e
        then putStrLn "Test Passed"
        else putStrLn "Test Failed"

    assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
    assertNotEq g e = if not (g == e)
        then putStrLn "Test Passed"
        else putStrLn "Test Failed"

    testDouble : IO ()
    testDouble = assertEq (double 2) 4

    testTriple : IO ()
    testTriple = assertNotEq (triple 2) 5


The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

    package maths

    modules = Maths.NumOps
            , Test.NumOps

    tests = Test.NumOps.testDouble
          , Test.NumOps.testTriple


The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

    > idris --testpkg maths.ipkg
    Type checking ./Maths/NumOps.idr
    Type checking ./Test/NumOps.idr
    Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
    Test Passed
    Test Passed

Note how both tests have reported success by printing ``Test Passed``
as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.