@@ -31,14 +31,18 @@ package file would be::
3131
3232
3333Other examples of package files can be found in the ``libs`` directory
34−of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
35−More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
34+of the main Idris repository, and in `third-party libraries
35+<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
3636
3737
3838Using Package files
3939===================
4040
41−Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
41+
42+Idris itself is aware about packages, and special commands are
43+available to help with, for example, building packages, installing
44+packages, and cleaning packages. For instance, given the ``maths``
45+package from earlier we can use Idris as follows:
4246
4347+ ``idris --build maths.ipkg`` will build all modules in the package
4448
@@ -48,20 +52,102 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile
4852+ ``idris --clean maths.ipkg`` will delete all intermediate code and
4953 executable files generated when building.
5054
51−+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
52− package in the folder ``maths_doc`` in your project's root
53− directory.
54−
55−+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
56− package only. This differs from build that type checks **and**
57− generates code.
58−
59−+ ``idris --testpkg maths.ipkg`` will compile and run any embedded
60− tests you have specified in the ``tests`` parameter. More
61− information about testing is given in the next section.
62−
6355Once the maths package has been installed, the command line option
6456``--package maths`` makes it accessible (abbreviated to ``-p maths``).
6557For example::
6658
6759 idris -p maths Main.idr
60+
61+
62+Testing Idris Packages
63+======================
64+
65+The integrated build system includes a simple testing framework.
66+This framework collects functions listed in the ``ipkg`` file under ``tests``.
67+All test functions must return ``IO ()``.
68+
69+
70+When you enter ``idris --testpkg yourmodule.ipkg``,
71+the build system creates a temporary file in a fresh environment on your machine
72+by listing the ``tests`` functions under a single ``main`` function.
73+It compiles this temporary file to an executable and then executes it.
74+
75+
76+The tests themselves are responsible for reporting their success or failure.
77+Test functions commonly use ``putStrLn`` to report test results.
78+The test framework does not impose any standards for reporting and consequently
79+does not aggregate test results.
80+
81+
82+For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
83+
84+.. name: Math/NumOps.idr
85+.. code-block:: idris
86+
87+ module Maths.NumOps
88+
89+ %access export -- to make functions under test visible
90+
91+ double : Num a => a -> a
92+ double a = a + a
93+
94+ triple : Num a => a -> a
95+ triple a = a + double a
96+
97+A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
98+
99+.. name: Math/TestOps.idr
100+.. code-block:: idris
101+
102+ module Test.NumOps
103+
104+ import Maths.NumOps
105+
106+ %access export -- to make the test functions visible
107+
108+ assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
109+ assertEq g e = if g == e
110+ then putStrLn "Test Passed"
111+ else putStrLn "Test Failed"
112+
113+ assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
114+ assertNotEq g e = if not (g == e)
115+ then putStrLn "Test Passed"
116+ else putStrLn "Test Failed"
117+
118+ testDouble : IO ()
119+ testDouble = assertEq (double 2) 4
120+
121+ testTriple : IO ()
122+ testTriple = assertNotEq (triple 2) 5
123+
124+
125+The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
126+The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
127+
128+ package maths
129+
130+ modules = Maths.NumOps
131+ , Test.NumOps
132+
133+ tests = Test.NumOps.testDouble
134+ , Test.NumOps.testTriple
135+
136+
137+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
138+
139+ > idris --testpkg maths.ipkg
140+ Type checking ./Maths/NumOps.idr
141+ Type checking ./Test/NumOps.idr
142+ Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
143+ Test Passed
144+ Test Passed
145+
146+Note how both tests have reported success by printing ``Test Passed``
147+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.
148+
149+More information
150+================
151+
152+More details, including a complete listing of available fields, can be
153+found in the reference manual in :ref:`ref-sect-packages`.