Packages — Idris 1.0 documentation

# 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. Package names can be any valid Idris identifier. The iPKG format also takes a quoted version that accepts any valid filename.
- 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.

### Metadata

From Idris v0.12 the iPKG format supports additional metadata associated with the package. The added fields are:

- `brief = "<text>"`, a string literal containing a brief description of the package.
- `version = <text>`, a version string to associate with the package.
- `readme = <file>`, location of the README file.
- `license = <text>`, a string description of the licensing information.
- `author = <text>`, the author information.
- `maintainer = <text>`, Maintainer information.
- `homepage = <url>`, the website associated with the package.
- `sourceloc = <url>`, the location of the DVCS where the source can be found.
- `bugtracker = <url>`, the location of the project’s bug tracker.

### Common Fields

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. Executable names can be any valid Idris identifier. the iPKG format also takes a quoted version that accepts any valid filename.
- `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 to be passed to Idris.
- `pkgs = <pkg name> (',' <pkg name>)+`, a comma separated list of package names that the Idris package requires.

### Binding to C

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 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 files to be installed (object files, headers), perhaps generated by the `Makefile`.

### Testing

For testing Idris packages there is a rudimentary testing harness, run in the `IO` context. 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.

Important

The modules containing the test functions must also be added to the list of modules.

### Comments

Package files support comments using the standard Idris singleline `--` and multiline `{- -}` format.

## 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.
- `idris --mkdoc test.ipkg` will build HTML documentation for your package in the folder `test_doc` in your project’s root directory.
- `idris --installdoc test.ipkg` will install the packages documentation into Idris’ central documentation folder located at `idris --docdir`.
- `idris --checkpkg test.ipkg` will type check all modules in the package only. This differs from build that type checks and generates code.
- `idris --testpkg test.ipkg` will compile and run any embedded tests you have specified in the `tests` parameter.

When building or install packages the commandline flag `--warnipkg` will audit the project and warn of any potentiable problems.

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