Skip to content

An Agda standard library website

Note

This is an experimental website, generated from the Agda source files in a FORK of the Agda standard library repository. It is a prototype of a potential replacement for the official Agda standard library website.

The website was generated and deployed from an unpublished branch of the fork after adding a Makefile, the mkdocs.yml configuration file, and a docs directory that includes some fixed auxiliary files, two Markdown files, and a small navigation panel specification file. See also the additional installation instructions.

The theme Material for MkDocs with the Awesome-Nav plugin generates the hierarchical navigation menus from the directory structure of the repository and the nav specification in the file docs/.nav.yml.

The README section contains all the modules from the doc/README directory.

The Library section contains the built-in modules, and standard library modules that are (transitively) imported by the index and README modules.

The HTML page is the root of the standard highlighted HTML pages generated by agda --html index.agda. Modulo the domain and version prefix, the URLs of the pages in the deployed website are the same as in the

The commands used to generate and browse this website are:1

make -f Makefile clean-all
make -f Makefile check
make -f Makefile web
make -f Makefile serve

Different versions of the generated website can be deployed using mike. The Makefile supports some simple commands for adding, updating, removing, and browsing deployed versions. The command to deploy version v to GitHub Pages is:

make -f Makefile deploy VERSION=v

The check command takes about 15 seconds (assuming that the library has previously been loaded). The web and serve commmands both take about 75 seconds, and deploy takes about 100 seconds.

The linkcheck application reports that the website has 2310 pages containing 2,310,253 internal links (ignoring (S)CSS links), all valid.

Warning

Search works best for websites where each page is divided into small sections. It is currently of limited use for websites generated from large Agda modules. Moreover, it appears that some ASCII characters do not produce the expected results (even when escaped by \).

Tip

Searching for foo bar returns the list of pages that contain foo and/or bar. To search for pages that contain both words, use +foo +bar, and +foo -bar for pages that contain foo but not bar.

Info

The rest of this file was copied from the README page of the official library repository.

The standard library aims to contain all the tools needed to write both programs and proofs easily. While we always try and write efficient code, we prioritize ease of proof over type-checking and normalization performance. If computational performance is important to you, then perhaps try agda-prelude instead.

Getting started

If you're looking to find your way around the library, there are several different ways to get started:

  • The library's structure and the associated design choices are described in the README.agda.

  • The README folder, which mirrors the structure of the main library, contains examples of how to use some of the more common modules. Feel free to open a new issue if there's a particular module you feel could do with some more documentation.

  • You can browse the library's source code in glorious clickable HTML.

Installation instructions

See the installation instructions for the latest version of the standard library.

Old versions of Agda

If you're using an old version of Agda, you can download the corresponding version of the standard library on the Agda wiki. The module index for older versions of the library is also available. For example, version 1.7 can be found at https://agda.github.io/agda-stdlib/v1.7/, just replace in the URL 1.7 with the version that you need.

Development version of Agda

If you're using a development version of Agda rather than the latest official release, you should use the experimental branch of the standard library rather than master. Instructions for updating the experimental branch. The experimental branch contains non-backward compatible patches for upcoming changes to the language.

Type-checking with flags

The --safe flag

Most of the library can be type-checked using the --safe flag. Please consult GenerateEverything.hs for a full list of modules that use unsafe features.

The --cubical-compatible flag

Most of the library can be type-checked using the --cubical-compatible flag, which since Agda v2.6.3 supersedes the former --without-K flag. Please consult GenerateEverything.hs for a full list of modules that use axiom K, requiring the --with-K flag.

Contributing to the library

If you would like to suggest improvements, feel free to use the Issues tab. Even better, if you would like to make the improvements yourself, we have instructions in HACKING to help you get started. For those who would simply like to help out, issues marked with the low-hanging-fruit tag are a good starting point.

  1. The option -f Makefile is required because make uses the existing GNUMakefile by default. The option will not be needed if the two files are merged. ↩