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.
15A package description includes the following:
17+ A header, consisting of the keyword package followed by the package name.
18+ Fields describing package contents, ``<field> = <value>``
20At least one field must be the modules field, where the value is a
21comma separated list of modules. For example, a library test which
22has two modules ``foo.idr`` and ``bar.idr`` as source files would be
29Other examples of package files can be found in the ``libs`` directory
30of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
35Other common fields which may be present in an ``ipkg`` file are:
37+ ``sourcedir = <dir>``, which takes the directory (relative to the
38 current directory) which contains the source. Default is the current
41+ ``executable = <output>``, which takes the name of the executable
44+ ``main = <module>``, which takes the name of the main module, and
45 must be present if the executable field is present.
47+ ``opts = "<idris options>"``, which allows options to be passed to
50+ ``pkgs = <pkg name> (',' <pkg name>)+``, a comma separated list of
51 package names that the Idris package requires.
56In more advanced cases, particularly to support creating bindings to
57external ``C`` libraries, the following options are available:
59+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
60 before the Idris modules, for example to support linking with a
63+ ``libs = <libs>``, which takes a comma separated list of libraries
64 which must be present for the package to be usable.
66+ ``objs = <objs>``, which takes a comma separated list of additional
67 object files to be installed, perhaps generated by the ``Makefile``.
72For testing Idris packages there is a rudimentary testing harness, run in the ``IO`` context.
73The ``iPKG`` file is used to specify the functions used for testing.
74The following option is available:
76+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
79 The modules containing the test functions must also be added to the list of modules.
84Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
86+ ``idris --build test.ipkg`` will build all modules in the package
88+ ``idris --install test.ipkg`` will install the package, making it
89 accessible by other Idris libraries and programs.
91+ ``idris --clean test.ipkg`` will delete all intermediate code and
92 executable files generated when building.
94+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
96+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
98+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.
100Once the test package has been installed, the command line option
101``--package test`` makes it accessible (abbreviated to ``-p test``).
104 idris -p test Main.idr
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list