Skip to content

Files

Latest commit

 

History

History
63 lines (50 loc) · 2.39 KB

installation-guide.md

File metadata and controls

63 lines (50 loc) · 2.39 KB

Installation instructions

Note: the full story on installing Agda libraries can be found at readthedocs.

Use version v2.2 of the standard library with Agda v2.7.0 or v2.7.0.1. You can find the correct version of the library to use for different Agda versions on the Agda Wiki.

  1. Navigate to a suitable directory $HERE (replace appropriately) where you would like to install the library.

  2. Download the tarball of v2.2 of the standard library. This can either be done manually by visiting the Github repository for the library, or via the command line as follows:

    wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.2.tar.gz

    Note that you can replace wget with other popular tools such as curl and that you can replace 2.2 with any other version of the library you desire.

  3. Extract the standard library from the tarball. Again this can either be done manually or via the command line as follows:

    tar -zxvf agda-stdlib.tar.gz

  4. [ OPTIONAL ] If using cabal then run the commands to install via cabal:

    cd agda-stdlib-2.2
cabal install

  5. Locate the file $AGDA_DIR/libraries where $AGDA_DIR on Ubuntu/MacOS can be found by running agda --print-agda-app-dir.

    Full details, including the various possible locations that $AGDA_DIR might map to, may be found in the online documentation.

    Note that the $AGDA_DIR directory and the libraries file within it, may not exist and you may have to create them.

  6. Register the standard library with Agda's package system by adding the following line to $AGDA_DIR/libraries:

    $HERE/agda-stdlib-2.2/standard-library.agda-lib

Now, the standard library is ready to be used either:

  • in your project $PROJECT, by creating a file $PROJECT.agda-lib in the project's root containing:

    depend: standard-library
include: $DIRS

    where $DIRS is a list of directories where Agda searches for modules, for instance . (just the project's root).

  • in all your projects, by adding the following line to $AGDA_DIR/defaults

    standard-library