git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/docs/tutorial/packages.rst
65 lines 2.3 kB history raw
1********
2Packages
3********
6Idris includes a simple build system for building packages and executables from a named package description file.
7These files can be used with the Idris compiler to manage the development process .
9Package Descriptions
10====================
12A package description includes the following:
14+ A header, consisting of the keyword package followed by the package name.
15+ Fields describing package contents, ``<field> = <value>``
17At least one field must be the modules field, where the value is a
18comma separated list of modules. For example, given an idris package
19``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
20``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
21package file would be::
23 package maths
25 modules = Maths
26 , Maths.NumOps
27 , Maths.BinOps
28 , Maths.HexOps
31Other examples of package files can be found in the ``libs`` directory
32of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
33More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
36Using Package files
37===================
39Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
41+ ``idris --build maths.ipkg`` will build all modules in the package
43+ ``idris --install maths.ipkg`` will install the package, making it
44 accessible by other Idris libraries and programs.
46+ ``idris --clean maths.ipkg`` will delete all intermediate code and
47 executable files generated when building.
49+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
50 package in the folder ``maths_doc`` in your project's root
51 directory.
53+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
54 package only. This differs from build that type checks **and**
55 generates code.
57+ ``idris --testpkg maths.ipkg`` will compile and run any embedded
58 tests you have specified in the ``tests`` paramater. More
59 information about testing is given in the next section.
61Once the maths package has been installed, the command line option
62``--package maths`` makes it accessible (abbreviated to ``-p maths``).
63For example::
65 idris -p maths Main.idr