Agda has a simple package management system to support working with multiple libraries in different locations. The central concept is that of a library.
Example: Using the standard library¶
Before we go into details, here is some quick information for the impatient on how to tell Agda about the location of the standard library, using the library management system.
Let’s assume you have downloaded the standard library into a directory which we
will refer to by
AGDA_STDLIB (as an absolute path). A library file
standard-library.agda-lib should exist in this directory, with the
name: standard-library include: src
To use the standard library by default in your Agda projects, you have to do two things:
Create a file
AGDA_DIR/librarieswith the following content:
(Of course, replace
AGDA_STDLIBby the actual path.)
~/.agdaon unix-like systems and
C:\Users\USERNAME\AppData\Roaming\agdaor similar on Windows. (More on
librariesfile informs Agda about the libraries you want it to know about.
Create a file
AGDA_DIR/defaultswith the following content:
defaultsfile informs Agda which of the libraries pointed to by
librariesshould be used by default (i.e. in the default include path).
That’s the short version, if you want to know more, read on!
A library consists of
- a name
- a set of dependencies
- a set of include paths
Libraries are defined in
.agda-lib files with the following syntax:
name: LIBRARY-NAME -- Comment depend: LIB1 LIB2 LIB3 LIB4 include: PATH1 PATH2 PATH3
Dependencies are library names, not paths to
.agda-lib files, and include
paths are relative to the location of the library-file.
To be found by Agda a library file has to be listed (with its full path) in a
AGDA_DIR/libraries-VERSION, or if that doesn’t exist
VERSION is the Agda version (for instance
AGDA_DIR defaults to
~/.agda on unix-like systems and
C:\Users\USERNAME\AppData\Roaming\agda or similar on Windows, and can be
overridden by setting the
AGDA_DIR environment variable.
Environment variables in the paths (of the form
expanded. The location of the libraries file used can be overridden using the
--library-file=FILE command line option.
You can find out the precise location of the
libraries file by
agda -l fjdsk Dummy.agda at the command line and looking at the
error message (assuming you don’t have a library called
Note that if you want to install a library so that it is used by default,
it must also be listed in the
defaults file (details below).
Using a library¶
There are three ways a library gets used:
You supply the
-l LIB) option to Agda. This is equivalent to adding a
-iPATHfor each of the include paths of
LIBand its (transitive) dependencies.
--libraryflag is given, and the current project root (of the Agda file that is being loaded) or one of its parent directories contains an
.agda-libfile defining a library
LIB. This library is used as if a
--library=LIBoption had been given, except that it is not necessary for the library to be listed in the
--libraryflag, and no
.agda-libfile in the project root. In this case the file
AGDA_DIR/defaultsis read and all libraries listed are added to the path. The
defaultsfile should contain a list of library names, each on a separate line. In this case the current directory is also added to the path.
To disable default libraries, you can give the flag
--no-default-libraries. To disable using libraries altogether, use the
If you want to usually use a variety of libraries, it is simplest to list them
all in the
AGDA_DIR/defaults file. It has format
standard-library library2 library3
where of course
library3 are the libraries you commonly use.
While it is safe to list all your libraries in
library, be aware that listing
libraries with name clashes in
defaults can lead to difficulties, and should be
done with care (i.e. avoid it unless you really must).
Library names can end with a version number (for instance,
When resolving a library name (given in a
--library flag, or listed as a
default library or library dependency) the following rules are followed:
- If you don’t give a version number, any version will do.
- If you give a version number an exact match is required.
- When there are multiple matches an exact match is preferred, and otherwise the latest matching version is chosen.
For example, suppose you have the following libraries installed:
otherlib-2.3. In this case, aside from
the exact matches you can also say
--library=otherlib to get
If you are upgrading from a pre 2.5 version of Agda, be aware that you may have
remnants of the previous library management system in your preferences. In particular,
if you get warnings about
agda2-include-dirs, you will need to find where this is
defined. This may be buried deep in
.el files, whose location is both operating
system and emacs version dependant.