v2.3, patched for Agda 2.9.0

agda-stdlib v2.3 with the five changes it needs to type-check under Agda 2.9.0, which no release carries yet. The formalverification projects pin it while they run Agda 2.9.0 at agda/agda da66a8c75f11d10699a6b38b261efdf244b66f2a, until Agda 2.9.0 and a standard library for it are released.

The changes, on top of v2.3 (8326c7475af1fa456ca04a0203c168d5d7ff842b), are as follows:

• 0297f4a7: agda-master's 1896499f, unchanged: eta equality is no longer inferred (agda/agda#8533).
• 1d7e2dae: agda-master's 1b7f26af, unchanged: fixity declarations for closed operators removed.
• f69293c1: agda-master's 39631ce9, ported to v2.3 by hand: irrelevant-recompute moves to a new module, Relation.Nullary.Recomputable.Unsafe.
• cb783289: master's fbf6ce16 (agda#2932), unchanged: a record pattern in Data.Nat.Primality, since instance search no longer eta-expands record variables (agda#2931).
• fb5d1840: master's b0d29e13 (agda#2935), unchanged: the same in Data.Nat.Primality and Data.Nat.PseudoRandom.LCG.

Checked: the whole library type-checks under Agda 2.9.0 at da66a8c: all 1,154 modules from source with agda --build-library, exit 0, in 111 s, the only warnings the library's own 50 deprecations (2026-10-07). Its standard-library.agda-lib still declares standard-library-2.3, so a library that depends on standard-library-2.3 needs no change.

Pinning it in a Nix flake

pkgs.fetchFromGitHub {
  owner = "formalverification";
  repo  = "agda-stdlib";
  rev   = "fb5d1840d26909038b5ae1459733b0db425a7488";
  hash  = "sha256-ZF+/2bUhKggpGY0WtHqKkOstRTGe8LOhK4lD+4T3xSc=";
}

Pin the commit, not the tag's name: a tag can be moved, a commit cannot. To use it as nixpkgs' standard library, override src (and version, for example "2.3-agda-2.9.0") of agdaPackages.standard-library, in a package set whose Agda is 2.9.0.

Getting the hash again

The hash is the NAR hash of the unpacked tree. Either of two ways gives it:

• Ask Nix: nix flake prefetch --json github:formalverification/agda-stdlib/<rev> | jq -r .hash.
• Let a build tell you: put hash = lib.fakeHash; in the hash's place, run nix build, and copy the hash the error prints after got: into the flake.

Both gave sha256-ZF+/2bUhKggpGY0WtHqKkOstRTGe8LOhK4lD+4T3xSc= on 2026-10-07, and a fetchFromGitHub with it fetched exactly the tree that passed the check above. The second way is also the fix whenever a build stops with hash mismatch in fixed-output derivation. For this commit a mismatch should never happen, since the tree of a pinned commit does not change, so look at what changed before you accept a new hash.

The tag first pointed, for half an hour on 2026-10-07, at f69293c1, before the whole library had been checked; nothing pinned it then.