Packages

Idris (from version 0.9.4) includes a simple system for building packages from a package description file (extension .ipkg). Given a package file test.ipkg:

  • 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).

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 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.