agda-algebras corpus v0.1

An agda-strux JSONL corpus of the whole of ualib/agda-algebras: one row per definition, carrying the definition's normalized name, its pretty-printed type, a structural encoding of that type, its dependency tokens, and its proof term where it has one.

v0.1 is a re-cut of v0 at a newer library commit: the pin the #127 benchmark tier is mined from, carrying the FLRP Kurzweil-surjectivity theorem (ualib/agda-algebras#569). Read the dataset card before using it, in particular its known-gaps section.

What is in this release

Asset	What it is
corpus.jsonl.gz	The corpus: 13,123 rows, 224,646,301 bytes uncompressed
coverage.json	Every module's extraction outcome, individually
provenance.json	Library commit, toolchain pins, run configuration, digests
stats.json / stats.md	Summary statistics, machine-readable and as tables
DATASET_CARD.md	The dataset card, as published in the repository

Provenance

• Source: ualib/agda-algebras at 4662373d281daf0f20a6319f1a46755a45d33293, working tree clean.
• Toolchain: Agda 2.8.0, standard library 2.3, GHC 9.10.3, pinned by flake.lock (nixpkgs-agda at 9dcb002ca1690658be4a04645215baea8b95f31d).
• Producer: formalverification/agda-native-air at ba9272a7fdda4002bdc2e0f9d3eec88865965f9c, via struxdriver.extract.AgdaJsonlDriver → agda-json. Recorded by the extraction itself, not sampled when the corpus was packaged.
• Row schema: agda-strux Full JSONL, docs/representation.md §3, typeAstVersion 0.3-v0 on every row.

Digests, confirmed byte-identical across two independent extraction runs and three assemblies:

corpus.jsonl     sha256  af8644328352d95cb2887dd553e4f23c0d1b807c1dcd1f6274aa4f8150e7ed35
corpus.jsonl.gz  sha256  a56785dc67df0e2a165a0cc3654c27e2357b98b26651c2d59bc3b7634d4fa1e2

Coverage

The library has 407 committed source modules, plus two Everything* barrels generated by its own Makefile (git-ignored upstream, present in the extraction checkout), so the scan enumerated 409 modules; all 409 were extracted and all 409 succeeded; 63 of them are barrels that contribute no definitions of their own. Nothing is excluded. coverage.json records each outcome with its row count, duration, and any validation error.

Contents

13,123 definitions across 779 distinct prettyModule values and 8 top-level namespaces; 12,027 carry a proof term. 12,161 functions, 649 constructors, 184 records, 126 data types. At definition level the graph is keyed by prettyQname: 11,865 nodes into which the 13,123 rows collapse, 53,687 dependency tokens naming a definition in the corpus, and 78,068 occurrences naming none; these are reported as unresolved tokens rather than as external edges, and 41,702 of them at least have the shape of a qualified name. Full tables are in stats.md.

Mind the tail: twelve rows exceed a megabyte (machine-generated certificate and table rows in FLRP and Examples; the largest is 11.5 MB), and the largest ten are 25.9 % of the corpus by bytes. Filter on body length before budgeting per row.

Using it

gunzip -k corpus.jsonl.gz
agda-mcp --corpus corpus.jsonl

That registers search_by_name, search_by_type, and get_dependencies; make corpus-mcp-smoke CORPUS_VERSION=v0.1 drives all three over the real JSON-RPC transport against this cut.

Reproducing it

git -C ~/git/ualib/agda-algebras/master checkout 4662373d281daf0f20a6319f1a46755a45d33293
make extract-lib-nix AGDA_ALGEBRAS_ROOT=~/git/ualib/agda-algebras/master RESUME=0
make corpus-nix CORPUS_VERSION=v0.1

Output is byte-identical for the same library commit and toolchain: modules concatenate in sorted order and the gzip carries no stored filename and mtime=0. Compare against the digests above. Expect six to seven minutes of wall time with warm .agdai interfaces.

License

The rows are derived from agda-algebras' src/, licensed Apache-2.0, Copyright 2025-2026 William DeMeo and Contributors, and are distributed under that license. Cite the library as the source of the mathematics:

The Agda Universal Algebra Library (ualib/agda-algebras), commit 4662373d281daf0f20a6319f1a46755a45d33293, Apache-2.0.

The dataset card and this notes page are CC-BY-4.0 (LICENSE-docs); stats.json/stats.md travel with the corpus under Apache-2.0.

agda-algebras corpus v0

An agda-strux JSONL corpus of the whole of ualib/agda-algebras: one row per definition, carrying the definition's normalized name, its pretty-printed type, a structural encoding of that type, its dependency tokens, and its proof term where it has one.

Read the dataset card before using it — in particular its known-gaps section.

What is in this release

Asset	What it is
corpus.jsonl.gz	The corpus: 11,666 rows, 184,904,547 bytes uncompressed
coverage.json	Every module's extraction outcome, individually
provenance.json	Library commit, toolchain pins, run configuration, digests
stats.json / stats.md	Summary statistics, machine-readable and as tables
DATASET_CARD.md	The dataset card, as published in the repository

Provenance

• Source: ualib/agda-algebras at ecc158a3730259b75d2ace4f5e30764e1c514380, working tree clean.
• Toolchain: Agda 2.8.0, standard library 2.3, GHC 9.10.3, pinned by flake.lock (nixpkgs-agda at 9dcb002ca1690658be4a04645215baea8b95f31d).
• Producer: formalverification/agda-native-air at 81df40c1c194919880860cff937f06ca3dcbbf12, via struxdriver.extract.AgdaJsonlDriver → agda-json. Recorded by the extraction itself, not sampled when the corpus was packaged.
• Row schema: agda-strux Full JSONL, docs/representation.md §3, typeAstVersion 0.3-v0 on every row.

Digests:

corpus.jsonl     sha256  acdfaa5766ed83c5055b5f9fee8a9eaeeeadbe4e98630d916352a7851845ed54
corpus.jsonl.gz  sha256  88bfd57097d98b3cc455b63899f191b312f3acc40f277cfe93fb40d5fac23238

Coverage

Every one of the library's 377 source files is a module, all 377 were extracted, and all 377 succeeded; 61 of them are barrels that contribute no definitions of their own. Nothing is excluded. coverage.json records each outcome with its row count, duration, and any validation error.

Contents

11,666 definitions across 702 distinct prettyModule values and 8 top-level namespaces; 10,629 carry a proof term. 10,748 functions, 625 constructors, 165 records, 125 data types. At definition level the graph is keyed by prettyQname: 10,520 nodes into which the 11,666 rows collapse, 47,202 dependency tokens naming a definition in the corpus, and 69,651 occurrences naming none — reported as unresolved tokens rather than as external edges, since 32,367 of them are bound variables or truncations that could not name anything anywhere. Full tables are in stats.md.

Using it

gunzip -k corpus.jsonl.gz
agda-mcp --corpus corpus.jsonl

That registers search_by_name, search_by_type, and get_dependencies. The corpus loads in about 1.4 s to a 308 MB resident footprint.

Reproducing it

git -C ~/git/ualib/agda-algebras/master checkout ecc158a3730259b75d2ace4f5e30764e1c514380
make extract-lib-nix AGDA_ALGEBRAS_ROOT=~/git/ualib/agda-algebras/master PAR=8 RESUME=0
make corpus-nix

Output is byte-identical for the same library commit and toolchain: modules concatenate in sorted order and the gzip carries no stored filename and mtime=0. Compare against the digests above.

License

The rows are derived from agda-algebras' src/, licensed Apache-2.0, Copyright 2025-2026 William DeMeo and Contributors, and are distributed under that license. Cite the library as the source of the mathematics:

The Agda Universal Algebra Library (ualib/agda-algebras), commit ecc158a3730259b75d2ace4f5e30764e1c514380, Apache-2.0.

The dataset card and the statistical summaries are CC-BY-4.0 (LICENSE-docs).