Packages¶
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.
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>
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
Foo.idr
and 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 0
.
Other examples of package files can be found in the libs
directory
of the main Idris repository, and in third-party libraries.
Metadata¶
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.1.0
,0.3.0
,3.1.4.1.5
etc)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.
Directories¶
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.
Common Fields¶
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/exec
by default. The location can be changed by specifying theoutputdir
field.main = <module>
, which takes the name of the main module, and must be present if theexecutable
field 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. Thepkg_description
is 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
(no constraints)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)
Comments¶
Package files support comments using the standard Idris singleline --
and multiline {- -}
format.
Using Package files¶
Given an Idris package file test.ipkg
it can be used with the Idris compiler as follows:
idris2 --build test.ipkg
will build all modules in the packageidris2 --install test.ipkg
will install the package to the global Idris library directory (that is$PREFIX/idris-<version>/
), making the modules in itsmodules
field accessible by other Idris libraries and programs. Note that this doesn’t install any executables, just library modules.idris2 --clean test.ipkg
will clean the intermediate build files.
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
Where does Idris look for packages?¶
Packages can be installed globally (under $PREFIX/idris-<version>/
as
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
$PREFIX/idris-<version>/pkgname-version
.
In each case, if more than one version satisfies the constraint, it will choose the one with the highest version number.