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

Updated package documentation.

Browse Source 
+ Documented testing
+ Documented the complete CLI for packages.
This commit is contained in:
Jan de Muijnck-Hughes 2015-06-23 08:36:05 +01:00
parent 0b68452037
commit 4ac4488461
1 changed files with 20 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
docs/tutorial/packages.rst
View File

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