Idris includes a 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 programs and packages.
A package description includes the following:
- A header, consisting of the keyword
packagefollowed 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>
Packages can describe libraries, executables, or both, and should include
a version number. For library packages,
one field must be the modules field, where the value is a comma separated list
of modules to be installed. For example, a library
test which has two modules
Bar.idr as source files would be written as follows:
package test version = 0.1 modules = Foo, Bar
When installed, this will be in a directory
test-0.1. If the version
number is missing, it will default to
Other examples of package files can be found in the
of the main Idris repository, and in third-party libraries.
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 = <version number>, a version number, which must be in the form of integers separated by dots (e.g.
readme = "<file>", location of the README file.
license = "<text>", a string description of the licensing information.
authors = "<text>", the author information.
maintainers = "<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.
sourcedir = "<dir>", the directory to look for Idris source files.
builddir = "<dir>", the directory to put the checked modules and the artefacts from the code generator.
outputdir = "<dir>", the directory where the code generator should output the executable.
Other common fields which may be present in an
ipkg file are:
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.
Executables are placed in
build/execby default. The location can be changed by specifying the
main = <module>, which takes the name of the main module, and must be present if the
executablefield is present.
opts = "<idris options>", which allows options to be passed to Idris.
depends = <pkg description> (',' <pkg description>)+, a comma separated list of package names that the Idris package requires. The
pkg_descriptionis the package name, followed by an optional list of version constraints. Version constraints are separated by
&&and can use operators
==. For example, the following are valid package descriptions:
contrib == 0.3.0(an exact version constraint)
contrib >= 0.3.0(an inclusive lower bound)
contrib >= 0.3.0 && < 0.4(an inclusive lower bound, and exclusive upper bound)
Using Package files¶
Given an Idris package file
test.ipkg it can be used with the Idris compiler as follows:
idris2 --build test.ipkgwill build all modules in the package
idris2 --install test.ipkgwill install the package to the global Idris library directory (that is
$PREFIX/idris-<version>/), making the modules in its
modulesfield accessible by other Idris libraries and programs. Note that this doesn’t install any executables, just library modules.
idris2 --clean test.ipkgwill clean the intermediate build files.
Once the test package has been installed, the command line option
--package test makes it accessible (abbreviated to
idris -p test Main.idr
Where does Idris look for packages?¶
Packages can be installed globally (under
described above) or locally (under a
depends subdirectory in the top level
working directory of a project).
Packages specified using
-p pkgname or with the
depends field of a
package will then be located as follows:
- First, Idris looks in
depends/pkgname-version, for a package which satsifies the version constraint.
- If no package is found locally, Idris looks in
In each case, if more than one version satisfies the constraint, it will choose the one with the highest version number.