Skip to content

usage.adoc

Latest commit

 

History

History
57 lines (44 loc) · 2.05 KB

usage.adoc

File metadata and controls

57 lines (44 loc) · 2.05 KB
Raw

Using Mathesis

This guide is for a reader who wants to find proofs in the estate, or an agent that needs a small, sourced context. To work on Mathesis itself, see contributing.

Read the atlas

The views are generated files; read them in place.

  • docs/atlas/generated/catalogue.adoc: one row for each repository with proof files of its own, split into theory and engineering.

  • docs/atlas/generated/az.adoc and organisations.adoc: the same rows by name and by owner.

  • docs/atlas/generated/registry.adoc: theorem-level claims, each with the grade that the canon reader derives from its home’s receipt.

  • docs/atlas/generated/bridges.adoc: candidate relations between two repositories.

  • docs/atlas/generated/index.json: the rows as one I-JSON/JCS document.

Find a source

find lists the rows that match every word of a query, in repository name, class, provers or status document.

bun scripts/atlas/census-atlas.mjs find agda

The output is a JSON array of rows (57 for agda on 2026-11-11).

Build a bounded context

context returns the matching rows as a JSON document no longer than MATHESIS_CONTEXT_CHARS characters (default 5000). It always carries a caveat that counts are not verification.

MATHESIS_CONTEXT_CHARS=1200 bun scripts/atlas/census-atlas.mjs context lean

Limits

  • Counts are textual: the census finds declarations by keyword, and holes and axioms by pattern. The kernel of each home repository is the authority.

  • A row is as fresh as its censused_at time; the source commit is in commit.

  • The frame holds public repositories only. Private repositories are a count in docs/atlas/census/private-count.json.

  • No grade in the atlas is typed by hand. A theorem without a receipt that the canon reader accepts reads ungraded.