@@ -31,14 +31,14 @@ of the main Idris repository, and in `third-party libraries <https://github.com/
32Other common fields which may be present in an ``ipkg`` file are:
32Other common fields which may be present in an ``ipkg`` file are:
34−+ ``sourcedir = <dir>``, which gives the directory (relative to the
34++ ``sourcedir = <dir>``, which takes the directory (relative to the
35 current directory) which contains the source. Default is the current
35 current directory) which contains the source. Default is the current
36 directory.
36 directory.
38−+ ``executable = <output>``, which gives the name of the executable
38++ ``executable = <output>``, which takes the name of the executable
39 file to generate.
39 file to generate.
41−+ ``main = <module>``, which gives the name of the main module, and
41++ ``main = <module>``, which takes the name of the main module, and
42 must be present if the executable field is present.
42 must be present if the executable field is present.
44+ ``opts = "<idris options>"``, which allows options (such as other
44+ ``opts = "<idris options>"``, which allows options (such as other
@@ -51,12 +51,21 @@ external ``C`` libraries, the following options are available:
51 before the Idris modules, for example to support linking with a
51 before the Idris modules, for example to support linking with a
52 ``C`` library.
52 ``C`` library.
54−+ ``libs = <libs>``, which gives a comma separated list of libraries
54++ ``libs = <libs>``, which takes a comma separated list of libraries
55 which must be present for the package to be usable.
55 which must be present for the package to be usable.
57−+ ``objs = <objs>``, which gives a comma separated list of additional
57++ ``objs = <objs>``, which takes a comma separated list of additional
58 object files to be installed, perhaps generated by the ``Makefile``.
58 object files to be installed, perhaps generated by the ``Makefile``.
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.
64++ ``tests = <test functions>``, which takes the qualified names of all tests to be run.
67+ The tests must also be added to the list of modules in ``modules``.
60Using Package files
69Using Package files
61===================
70===================
@@ -70,6 +79,12 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler
70+ ``idris --clean test.ipkg`` will delete all intermediate code and
79+ ``idris --clean test.ipkg`` will delete all intermediate code and
71 executable files generated when building.
80 executable files generated when building.
82++ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
84++ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
86++ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.
73Once the test package has been installed, the command line option
88Once the test package has been installed, the command line option
74``--package test`` makes it accessible (abbreviated to ``-p test``).
89``--package test`` makes it accessible (abbreviated to ``-p test``).
75For example::
90For example::