idris-0.12.3: docs/tutorial/packages.rst
********
Packages
********
Idris includes a simple build system for building packages and executables from a named package description file.
These files can be used with the Idris compiler to manage the development process .
Package Descriptions
====================
A package description includes the following:
+ A header, consisting of the keyword package followed by the package
name. Package names can be any valid Idris identifier. The iPKG
format also takes a quoted version that accepts any valid filename.
+ Fields describing package contents, ``<field> = <value>``
At least one field must be the modules field, where the value is a
comma separated list of modules. For example, given an idris package
``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
package file would be::
package maths
modules = Maths
, Maths.NumOps
, Maths.BinOps
, Maths.HexOps
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>`_.
More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
Using Package files
===================
Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
+ ``idris --build maths.ipkg`` will build all modules in the package
+ ``idris --install maths.ipkg`` will install the package, making it
accessible by other Idris libraries and programs.
+ ``idris --clean maths.ipkg`` will delete all intermediate code and
executable files generated when building.
+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
package in the folder ``maths_doc`` in your project's root
directory.
+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
package only. This differs from build that type checks **and**
generates code.
+ ``idris --testpkg maths.ipkg`` will compile and run any embedded
tests you have specified in the ``tests`` parameter. More
information about testing is given in the next section.
Once the maths package has been installed, the command line option
``--package maths`` makes it accessible (abbreviated to ``-p maths``).
For example::
idris -p maths Main.idr