ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

Updated package documentation.

Browse Source
This commit is contained in:
Jan de Muijnck-Hughes 2015-06-23 09:26:29 +01:00
parent 6923b5451a
commit 8b46d8f138
1 changed files with 14 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
docs/tutorial/packages.rst
View File

@ -29,6 +29,9 @@ written as follows::
Other examples of package files can be found in the ``libs`` directory
of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
Common Fields
-------------
Other common fields which may be present in an ``ipkg`` file are:
+ ``sourcedir = <dir>``, which takes the directory (relative to the
@ -44,6 +47,9 @@ Other common fields which may be present in an ``ipkg`` file are:
+ ``opts = "<idris options>"``, which allows options (such as other
packages) to be passed to Idris.
Binding to C
------------
In more advanced cases, particularly to support creating bindings to
external ``C`` libraries, the following options are available:
@ -57,14 +63,17 @@ external ``C`` libraries, the following options are available:
+ ``objs = <objs>``, which takes a comma separated list of additional
object files to be installed, perhaps generated by the ``Makefile``.
For testing Idris packages, there is a rudimentary testing harness built into Idris.
This allows for testing functions that are written in context of ``IO`` to be run automatically in a fresh environment on your computer.
The field is:
Testing
--------
+ ``tests = <test functions>``, which takes the qualified names of all tests to be run.
For testing Idris packages, there is a rudimentary testing harness, which is run in the ``IO`` context, built into Idris.
This allows for testing modules containting functions that test aspects of your package to be run automatically in a fresh environment on your computer.
All test functions must return ``IO ()``, and are listed in the ``ipkg`` file using the field:
+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
.. IMPORTANT::
The tests must also be added to the list of modules in ``modules``.
The modules containing the test functions must also be added to the list of modules.
Using Package files
===================