Idris includes a simple system for building packages from a package description file. These files can be used with the Idris compiler to manage the development process of your Idris programmes and packages.
A package description includes the following:
- A header, consisting of the keyword package followed by the package name.
- 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, a library test which
has two modules
bar.idr as source files would be
written as follows:
package foo modules = foo, bar
Other examples of package files can be found in the
of the main Idris repository, and in third-party libraries.
Other common fields which may be present in an
ipkg file are:
sourcedir = <dir>, which takes the directory (relative to the current directory) which contains the source. Default is the current directory.
executable = <output>, which takes the name of the executable file to generate.
main = <module>, which takes the name of the main module, and must be present if the executable field is present.
opts = "<idris options>", which allows options (such as other packages) to be passed to Idris.
Binding to C¶
In more advanced cases, particularly to support creating bindings to
C libraries, the following options are available:
makefile = <file>, which specifies a
Makefile, to be built before the Idris modules, for example to support linking with a
libs = <libs>, which takes a comma separated list of libraries which must be present for the package to be usable.
objs = <objs>, which takes a comma separated list of additional object files to be installed, perhaps generated by the
For testing Idris packages there is a rudimentary testing harness, run in the
iPKG file is used to specify the functions used for testing.
The following option is available:
tests = <test functions>, which takes the qualified names of all test functions to be run.
The modules containing the test functions must also be added to the list of modules.
Using Package files¶
Given an Idris package file
text.ipkg it can be used with the Idris compiler as follows:
idris --build test.ipkgwill build all modules in the package
idris --install test.ipkgwill install the package, making it accessible by other Idris libraries and programs.
idris --clean test.ipkgwill delete all intermediate code and executable files generated when building.
idris --mkdoc test.ipkgwill build HTML documentation for your package in the folder
test_docin your project’s root directory.
idris --checkpkg test.ipkgwill type check all modules in the package only. This differs from build that type checks and generates code.
idris --testpkg test.ipkgwill compile and run any embedded tests you have specified in the
Once the test package has been installed, the command line option
--package test makes it accessible (abbreviated to
idris -p test Main.idr