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 a Makefile, to be built before the Idris modules, for example to support linking with a C 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 the Makefile.

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 package
  • idris --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