git.iko.soy/Idris-dev
on f0a67ff help sign in
Idris-dev/docs/reference/packages.rst
137 lines 4.6 kB history raw
1.. _ref-sect-packages:
3********
4Packages
5********
7Idris includes a simple system for building packages from a
8package description file. These files can be used with the Idris
9compiler to manage the development process of your Idris
10programmes and packages.
12Package Descriptions
13====================
15A package description includes the following:
17+ A header, consisting of the keyword package followed by the package
18 name. Package names can be any valid Idris identifier. The iPKG
19 format also takes a quoted version that accepts any valid filename.
20+ Fields describing package contents, ``<field> = <value>``
22At least one field must be the modules field, where the value is a
23comma separated list of modules. For example, a library test which
24has two modules ``foo.idr`` and ``bar.idr`` as source files would be
25written as follows::
27 package foo
29 modules = foo, bar
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>`_.
34Metadata
35--------
37From Idris `v0.12` the `iPKG` format supports additional metadata
38associated with the package.
39The added fields are:
41+ ``brief = "<text>"``, a string literal containing a brief description
42 of the package.
44+ ``version = <text>``, a version string to associate with the package.
46+ ``readme = <file>``, location of the README file.
48+ ``license = <text>``, a string description of the licensing
49 information.
51+ ``author = <text>``, the author information.
53+ ``maintainer = <text>``, Maintainer information.
55+ ``homepage = <url>``, the website associated with the package.
57+ ``sourceloc = <url>``, the location of the DVCS where the source
58 can be found.
60+ ``bugtracker = <url>``, the location of the project's bug tracker.
63Common Fields
64-------------
66Other common fields which may be present in an ``ipkg`` file are:
68+ ``sourcedir = <dir>``, which takes the directory (relative to the
69 current directory) which contains the source. Default is the current
70 directory.
72+ ``executable = <output>``, which takes the name of the executable
73 file to generate. Executable names can be any valid Idris
74 identifier. the iPKG format also takes a quoted version that accepts
75 any valid filename.
77+ ``main = <module>``, which takes the name of the main module, and
78 must be present if the executable field is present.
80+ ``opts = "<idris options>"``, which allows options to be passed to
81 Idris.
83+ ``pkgs = <pkg name> (',' <pkg name>)+``, a comma separated list of
84 package names that the Idris package requires.
86Binding to C
87------------
89In more advanced cases, particularly to support creating bindings to
90external ``C`` libraries, the following options are available:
92+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
93 before the Idris modules, for example to support linking with a
94 ``C`` library.
96+ ``libs = <libs>``, which takes a comma separated list of libraries
97 which must be present for the package to be usable.
99+ ``objs = <objs>``, which takes a comma separated list of additional
100 object files to be installed, perhaps generated by the ``Makefile``.
102Testing
103--------
105For testing Idris packages there is a rudimentary testing harness, run in the ``IO`` context.
106The ``iPKG`` file is used to specify the functions used for testing.
107The following option is available:
109+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
111.. IMPORTANT::
112 The modules containing the test functions must also be added to the list of modules.
114Using Package files
115===================
117Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
119+ ``idris --build test.ipkg`` will build all modules in the package
121+ ``idris --install test.ipkg`` will install the package, making it
122 accessible by other Idris libraries and programs.
124+ ``idris --clean test.ipkg`` will delete all intermediate code and
125 executable files generated when building.
127+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
129+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
131+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.
133Once the test package has been installed, the command line option
134``--package test`` makes it accessible (abbreviated to ``-p test``).
135For example::
137 idris -p test Main.idr