Packages¶
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.
Package Descriptions¶
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 foo.idr
and 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 libs
directory
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 gives the directory (relative to the current directory) which contains the source. Default is the current directory.executable = <output>
, which gives the name of the executable file to generate.main = <module>
, which gives 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.
In more advanced cases, particularly to support creating bindings to
external C
libraries, the following options are available:
makefile = <file>
, which specifies aMakefile
, to be built before the Idris modules, for example to support linking with aC
library.libs = <libs>
, which gives a comma separated list of libraries which must be present for the package to be usable.objs = <objs>
, which gives a comma separated list of additional object files to be installed, perhaps generated by theMakefile
.
Using Package files¶
Given an Idris package file text.ipkg
it can be used with the Idris compiler as follows:
idris --build test.ipkg
will build all modules in the packageidris --install test.ipkg
will install the package, making it accessible by other Idris libraries and programs.idris --clean test.ipkg
will delete all intermediate code and executable files generated when building.
Once the test package has been installed, the command line option
--package test
makes it accessible (abbreviated to -p test
).
For example:
idris -p test Main.idr