git.iko.soy/Idris-dev
on f0a67ff help sign in
Idris-dev/docs/tutorial/packages.rst
67 lines 2.4 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
15 name. Package names can be any valid Idris identifier. The iPKG
16 format also takes a quoted version that accepts any valid filename.
17+ Fields describing package contents, ``<field> = <value>``
19At least one field must be the modules field, where the value is a
20comma separated list of modules. For example, given an idris package
21``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
22``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
23package file would be::
25 package maths
27 modules = Maths
28 , Maths.NumOps
29 , Maths.BinOps
30 , Maths.HexOps
33Other examples of package files can be found in the ``libs`` directory
34of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
35More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
38Using Package files
39===================
41Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
43+ ``idris --build maths.ipkg`` will build all modules in the package
45+ ``idris --install maths.ipkg`` will install the package, making it
46 accessible by other Idris libraries and programs.
48+ ``idris --clean maths.ipkg`` will delete all intermediate code and
49 executable files generated when building.
51+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
52 package in the folder ``maths_doc`` in your project's root
53 directory.
55+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
56 package only. This differs from build that type checks **and**
57 generates code.
59+ ``idris --testpkg maths.ipkg`` will compile and run any embedded
60 tests you have specified in the ``tests`` parameter. More
61 information about testing is given in the next section.
63Once the maths package has been installed, the command line option
64``--package maths`` makes it accessible (abbreviated to ``-p maths``).
65For example::
67 idris -p maths Main.idr