on cd4e91d help sign in
Idris-dev/docs/tutorial/testing.rst
65 lines 2.1 kB history raw
1.. _tut-sect-testing:
3**********************
4Testing Idris Packages
5**********************
7As part of the integrated build system a simple testing framework is provided.
8This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.
9This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.
12It is up to the developer to ensure the correct reporting of test results, and the structure and nature of how the tests are run.
13Further, 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.
16For 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
20 module Maths.NumOps
22 double : Num a => a -> a
23 double a = a + a
25 triple : Num a => a -> a
26 triple a = a + double a
28A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
30.. code-block:: idris
32 module Test.NumOps
34 import Maths.NumOps
36 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
37 assertEq g e = if g == e
38 then putStrLn "Test Passed"
39 else putStrLn "Test failed"
41 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
42 assertNotEq g e = if not (g == e)
43 then putStrLn "Test Passed"
44 else putStrLn "Test failed"
46 testDouble : IO ()
47 testDouble = assertEq (double 2) 4
49 testTriple : IO ()
50 testTriple = assertNotEq (triple 2) 5
53The 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::
56 module maths
58 module = Maths.NumOps
59 , Test.NumOps
61 tests = Test.NumOps.testDouble
62 , Test.NumOps.testTriple
65The testing framework can be invoked using: ``idris --testpkg maths.ipkg``.