@@ -31,14 +31,14 @@ of the main Idris repository, and in `third-party libraries <https://github.com/
3131
3232Other common fields which may be present in an ``ipkg`` file are:
3333
34−+ ``sourcedir = <dir>``, which gives the directory (relative to the
34++ ``sourcedir = <dir>``, which takes the directory (relative to the
3535 current directory) which contains the source. Default is the current
3636 directory.
3737
38−+ ``executable = <output>``, which gives the name of the executable
38++ ``executable = <output>``, which takes the name of the executable
3939 file to generate.
4040
41−+ ``main = <module>``, which gives the name of the main module, and
41++ ``main = <module>``, which takes the name of the main module, and
4242 must be present if the executable field is present.
4343
4444+ ``opts = "<idris options>"``, which allows options (such as other
@@ -51,12 +51,21 @@ external ``C`` libraries, the following options are available:
5151 before the Idris modules, for example to support linking with a
5252 ``C`` library.
5353
54−+ ``libs = <libs>``, which gives a comma separated list of libraries
54++ ``libs = <libs>``, which takes a comma separated list of libraries
5555 which must be present for the package to be usable.
5656
57−+ ``objs = <objs>``, which gives a comma separated list of additional
57++ ``objs = <objs>``, which takes a comma separated list of additional
5858 object files to be installed, perhaps generated by the ``Makefile``.
5959
60+For testing Idris packages, there is a rudimentary testing harness built into Idris.
61+This allows for testing functions that are written in context of ``IO`` to be run automatically in a fresh environment on your computer.
62+The field is:
63+
64++ ``tests = <test functions>``, which takes the qualified names of all tests to be run.
65+
66+.. IMPORTANT::
67+ The tests must also be added to the list of modules in ``modules``.
68+
6069Using Package files
6170===================
6271
@@ -70,6 +79,12 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler
7079+ ``idris --clean test.ipkg`` will delete all intermediate code and
7180 executable files generated when building.
7281
82++ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
83+
84++ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
85+
86++ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.
87+
7388Once the test package has been installed, the command line option
7489``--package test`` makes it accessible (abbreviated to ``-p test``).
7590For example::