# agda-stdlib and the choice between fast proofs and fast code > The Agda standard library is the shared library that Agda proof developers build on, and it makes an explicit trade: ease of proof is prioritised over type-checking and normalisation performance. The README points computational work to agda-prelude instead, which tells you when not to use it. **agda/agda-stdlib** — The Agda standard library - Repository: https://github.com/agda/agda-stdlib - Website: https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary - Stars: 677 · Forks: 276 - Language: Agda - License: NOASSERTION - Published: 2026-10-21 · Updated: 2026-10-21 · Language: en - Canonical page: https://hysenlabs.com/projects/agda-agda-stdlib ## The library states its own priority order The project description is unusually direct about what it optimises for. It says the library aims to contain all the tools needed to write both programs and proofs easily, and that while the authors always try to write efficient code, they prioritise ease of proof over type-checking and normalisation performance. That single sentence is the design brief for everything else in the repository, and it has a direct consequence for the reader: this is the library to reach for when you are writing proofs, not when you are writing a program whose runtime behaviour you care about. For that second case the documentation names a specific alternative. If computational performance is important, it suggests trying agda-prelude instead. The difference in approach is not cosmetic. Both libraries provide the basic vocabulary of a dependently typed language, but agda-stdlib chooses the implementations that make proofs short and readable even when they normalise slowly, while the alternative is aimed at programs where evaluation cost matters. The repository reflects a mature project with a wide surface. There is a src directory holding the modules, a doc directory, a tests directory, a CHANGELOG directory alongside CHANGELOG.md, a Header file, and a set of stack configuration files for a long series of GHC versions from 8.0.2 up to 9.12.4, each with its own stack YAML file. The version numbering tracks releases such as v2.2, v2.3 and v2.4, with v2.4 published on 2026-06-17. ## Three documented ways into a library that has no single entry point Agda libraries are directories of modules, and there is no obvious front door, so the project page spends real effort on navigation. It offers three starting points. The first is README.agda in the doc directory, which describes the library's structure and the associated design choices. The second is the README folder, which mirrors the structure of the main library and holds examples of how to use the more common modules. The project asks readers to open an issue if a particular module feels in need of more documentation, which is a good signal about where the gaps are. The third is the generated HTML source browser at agda.github.io/agda-stdlib, described as clickable HTML. For a library of this size, being able to jump straight to a module and read its types is the difference between a few minutes of work and an afternoon of guessing. The homepage of the project points to the Agda wiki page for the standard library, and the older versioned module index pattern is documented too: version 1.7 is reachable at https://agda.github.io/agda-stdlib/v1.7/, with the instruction to replace 1.7 in the URL with the version you need. That URL scheme is worth knowing, because it lets you read the documentation of the library version that matches an older Agda release rather than guessing at the current one. ## The one line installer is labelled experimental On Unix-style systems the installation section says it should be as simple as running one command in a shell: ```shell sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)" ``` Note the heading above it: automated installation is marked as currently experimental. That qualifier matters for anyone about to wire this into a provisioning script. The command pipes a script fetched over the network straight into a shell, which is a pattern worth thinking about twice even when the source is the project itself, and the installation section does not describe what the script does to your Agda installation or how to undo it. The supported route is the manual one. The documentation points to the installation instructions in doc/installation-guide.md for the latest version, and that is the document to follow when you care about what ends up on disk. For older Agda versions, the answer is different again: download the corresponding version of the library from the Agda wiki. The repository also ships a standard-library.agda-lib file and an agda-stdlib-utils.cabal package, alongside a Setup.hs and a GNUmakefile, so parts of the library are usable with cabal as well as with Agda's own library manager. ## master and experimental track different Agda versions Two branches serve two different needs, and picking the wrong one costs you time. The default branch is master. If you are using a development version of Agda rather than the latest official release, the documentation says you should use the experimental branch instead, and points to doc/updating-experimental.txt for the instructions on how to update it. The reason is stated plainly: the experimental branch contains non-backward compatible patches for upcoming changes to the language. That is a strong statement. The library on that branch is deliberately allowed to break compatibility in order to prepare for language changes, so anything you build against it is pinned to a moving target. For production work, master is the sane choice, and experimental is for people tracking the language itself. The branch layout also shows up in the badges. Two Ubuntu build badges, one for the default branch and one explicitly pointed at the experimental branch, so both lines are built in continuous integration rather than one being an afterthought. The release tags are versioned separately from the branch: v2.2 on 2025-01-15, v2.3 on 2025-08-02 and v2.4 on 2026-06-17. The last push was on 2026-10-21, so commits are landing after the v2.4 tag and the master branch is ahead of the most recent release. ## Type-checking flags decide which modules you can use Agda's type checker accepts flags that restrict what a module is allowed to do, and the library is explicit about how it stands against them. Most of the library can be type-checked using the --safe flag, and GenerateEverything.hs holds the full list of modules that use unsafe features. The same pattern applies to axiom K. Most of the library can be type-checked using the --without-K flag, and again GenerateEverything.hs holds the list of modules that use axiom K and therefore require the --with-K flag. Both of these are line ranges in a single Haskell file, GenerateEverything.hs, one for the safe list and one for the axiom K list. That is a design decision with a practical effect: the constraint is not spread across hundreds of module headers, it is maintained in one place. The cost is that you cannot tell from a single import whether a module is safe, and you have to check the file when you hit an unexpected rejection. If your project needs the whole library to type-check under --safe without exceptions, that check is the first thing to do before you plan around it. The same applies to --without-K, which matters for projects that want to avoid axiom K in their trusted base. ## Licensing and the cost of adopting a shared proof base The repository does not use a licence identifier that GitHub can classify. The entry is recorded as a custom licence pointing at the LICENSE file, and the repository root contains a file named LICENCE. In practice this means the terms are not something a licence scanner will summarise for you, and anyone using this library in a commercial or published setting has to read that file rather than rely on a badge. Whether the terms suit your use is a question for your own legal review, not something the repository states. The upgrade cost of a standard library is different in kind from the upgrade cost of an application library. Because proof developments tend to depend on specific names, specific signatures and specific argument orders, a major version bump of the library can break a proof that was otherwise complete. The CHANGELOG.md file and the CHANGELOG directory are the record of those changes, and the tags v2.2, v2.3 and v2.4 mark the boundaries. There is a second cost that the repository itself makes visible. The library contains unsafe modules and modules that rely on axiom K, and those exceptions are enumerated in GenerateEverything.hs. A project that wants --safe everywhere has to accept either the listed exceptions or the work of avoiding those modules, and a project that wants --without-K has the same decision to make. That is a genuine constraint on adoption, and it is checkable before you commit to anything. For contributors, HACKING explains how to make the improvements yourself, and points to issues labelled low-hanging-fruit as a way to help without writing code. ## Conclusion agda-stdlib suits teams writing Agda proofs and small certified programs who want a maintained, well documented shared vocabulary. It is the wrong choice when computational performance dominates, because the library itself states that it prioritises ease of proof over type-checking and normalisation performance and points to agda-prelude for that case. Before adopting it, check the type-checking flags your project needs against GenerateEverything.hs, pick master or experimental to match your Agda version, and read the LICENCE file yourself because it is a custom licence. ## FAQ ### How do I install agda-stdlib on Unix systems? The installation section gives an automated install command, sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)", but the heading labels automated installation as currently experimental. The supported route is the manual installation guide in doc/installation-guide.md. ### What is the difference between agda-stdlib and agda-prelude? The agda-stdlib description says it prioritises ease of proof over type-checking and normalisation performance, and it points to agda-prelude for users whose priority is computational performance. ### Which agda-stdlib branch should I use with a development version of Agda? Use the experimental branch rather than master. The documentation states that the experimental branch contains non-backward compatible patches for upcoming changes to the language. ### Which modules of agda-stdlib are not safe or use axiom K? Most of the library can be type-checked with the --safe flag and with the --without-K flag. The modules that use unsafe features and the modules that use axiom K are listed in GenerateEverything.hs. ### What licence does agda-stdlib use? The project is recorded as using a custom licence that GitHub cannot classify, with the terms held in the LICENCE file at the repository root. The project page itself does not summarise the terms. ## Sources - [agda/agda-stdlib on GitHub](https://github.com/agda/agda-stdlib) - [Issues](https://github.com/agda/agda-stdlib/issues) - [Project website](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary) - [README](https://github.com/agda/agda-stdlib/blob/master/README.md) - [Releases](https://github.com/agda/agda-stdlib/releases) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/agda-agda-stdlib