← lean-pkg documentation

A catalog you can re-derive, or it isn’t a catalog.

The index is a public, forkable list of verified Lean packages. Each entry names a package repository at a pinned commit, says how far its evidence goes (its trust level), and carries verbatim copies of the receipts that justify that level. Anyone can re-derive an entry from the package’s bytes at the pin with one command. Everything is a file; git is the database.

Layout

index/
  README.md                         generated by `lean-pkg index render`; never hand-edited
  <name>/
    entry.yaml                      schema index-entry/2
    receipts/<c12>-<job>.json       verbatim copy of the lower-tier receipt
    receipts/<c12>-comparator.json  verbatim copy of the comparator receipt

Logs stay in the package repository (under .lean-receipts/); index check fetches them at the pin. The index root is --index PATH, else the environment variable LEAN_PKG_INDEX, else index/ beside the registry when it exists, else ./index, so the index can move to its own repository later without code changes. index check, render and migrate refuse (exit 1) a root that does not exist.

Trust levels

Trust Evidence that must validate at the pin Proves
lower-tier a lower-tier receipt (gate’s validator) the package builds with no sorry and only the standard axioms at that commit
comparator a comparator receipt (comparator --check’s validator) the named theorems match the trusted statements; the table shows the mechanism, and legacy is not predictive of Palomar acceptance
palomar a Palomar id, verified against data.palomar-registry.org when the network is reachable the result is registered in Palomar

What each level does not prove, and how to re-derive an entry without a registry, is in the Trust model.

Trust is computed, never typed: index add derives it from the evidence present, and index check recomputes it and refuses an entry whose stated trust differs from its evidence.

comparator trust also requires coverage: every headline theorem must name, in judged_as, a theorem that one of the comparator receipt’s configurations judged (a Challenge restates a theorem under its own name). A comparator receipt that judged other statements, such as a smoke configuration, does not grade the headline: the entry is lower-tier if a lower-tier receipt exists, and refused otherwise.

Entry schema (index-entry/2; index-entry/1 still validates)

Keys appear in exactly this order; an unknown key is refused. Every key is required except built_on, which index-entry/2 accepts as an optional key (proposal 0007); an entry without it stays valid. index add writes index-entry/2, which adds claims after headline; an index-entry/1 entry has no claims key and stays valid; lean-pkg index migrate rewrites it as index-entry/2 by deriving claims from its headline (no other key changes), so its headlines become searchable.

Key Value
schema index-entry/2 (or index-entry/1)
name the directory name
repo public https URL
pin commit (40 hex, the receipts’ commit) and tag (or null; at the pin or an evidence-only descendant, or a docs-only one when the registry record opts in; see below)
lean_toolchain equals lean-toolchain at the pin
mathlib_rev equals the Mathlib rev in lake-manifest.json at the pin, or null
license_spdx SPDX id; a license file must exist at the pin
trust lower-tier, comparator or palomar (computed)
receipts lower and comparator: repository paths under .lean-receipts/, or null
headline list of name (fully qualified), file (repository-relative .lean), summary (one sentence), and optionally judged_as (the Challenge theorem name under which a comparator configuration judged it)
claims index-entry/2 only: one claim per headline item, derived at index add and never typed: id (<name>/<slug of the declaration>), decl, kind (theorem), summary, judged_as, trust (the entry’s); lean-pkg search finds them (Prior-art search)
palomar list of id and version
doi null, or concept and versions (each doi, tag, commit)
reservoir null, or the package’s Reservoir page
formalization_yaml null, or a repository-relative path
built_on optional, index-entry/2 only: credits for third-party Lean code the package builds on (see Credits); omitted when there is none
fields lowercase tags such as probability
consent recorded (true or false); the pointers to the consent records stay private
added at (ISO-8601) and by (a public handle)
notes free text

No value may look like a local path, and local_path is never written.

Credits (built_on)

A package that is a thin layer over someone else’s library should say so where readers look: index render shows each credit in the Built on column of index/README.md (the library’s name linked to its repository, and its authors) and again in a Built on section with the relation, license, pin and note. built_on is a non-empty list; each credit is a mapping with these keys, in this order, and no others:

Key Value
name required: the library’s name, one line
url required: its public https repository URL
authors required: a non-empty list of names, as the library itself states its authorship (a file header, its README or CITATION.cff)
license optional: its SPDX expression
pin optional: the 40-hex commit the package uses
relation optional: depends-on (a Lake dependency in lake-manifest.json) or adapted-from (source copied into the package and modified)
note optional: one line, at most 300 characters, such as what the package takes from it

An optional key is omitted, never null. Credits are not evidence: they change neither trust nor the checks at the pin, and index check --clone only warns when a depends-on (or unlabelled) credit’s pin differs from the rev of the package with that URL in lake-manifest.json at the entry’s pin, or when no package there has that URL. An adapted-from credit is vendored source, so its pin is not compared.

What to list: every third-party Lean library the package’s Lean code imports or copies, from its lake-manifest.json (its direct requires and the libraries they pull in) and from any vendored source it carries. Mathlib and the packages Mathlib itself pulls in (Batteries, Aesop, Qq, ProofWidgets, Plausible, ImportGraph, LeanSearchClient, Cli), and code copied from Mathlib, are implicit and not listed; Lean core is not listed. Tools that are not Lean code the package builds on (scripts, CI helpers) are out of scope.

A missing credit for a Lake dependency is caught: index check --clone (or --repo-dir) reads lake-manifest.json at the entry’s pin and prints one note, “warning: Lake dependency NAME (URL) in lake-manifest.json at the pin has no built_on credit”, for each package in packages[] that is not implicit and that no credit names; --json lists them in the entry’s uncredited_dependencies (name and url; [] in a static check). A credit names a package when its url equals the package’s URL (ignoring case and a trailing .git) or its name equals the package’s name (ignoring case), whatever its relation. The warning never fails the check: the exit status and ok are unchanged. A package is implicit when

inherited alone does not make a package implicit: a library pulled in by a credited library is not Mathlib’s and warns until it is credited. A direct require from those two organizations that is not in the list (a tactic library, say) warns as well.

built_on:
- name: MarkovProcess
  url: https://github.com/scottnarmstrong/MarkovProcess
  authors:
  - Scott Armstrong
  license: Apache-2.0
  pin: 666cda029098a1106914fc9fa7abd1727573284a
  relation: depends-on
  note: Supplies the Brownian motion, exit times and Dynkin's formula.

Adding an entry

From your registry row (repository, receipts, license, Palomar ids, DOI and Reservoir listing are taken from it):

lean-pkg index add my-lean --from-registry --by your-handle \
  --headline 'MyLean.main_theorem :: MyLean/Main.lean :: One sentence saying what it proves.'

Without a registry, pass the facts as flags:

lean-pkg index add my-lean --repo https://github.com/you/my-lean --license Apache-2.0 \
  --lower .lean-receipts/0123456789ab-slurm-4242.json \
  --comparator .lean-receipts/0123456789ab-comparator.json \
  --by your-handle --headline 'MyLean.main_theorem :: MyLean/Main.lean :: One sentence.'
lean-pkg index render

Credits are given with --built-on-file FILE, a YAML file holding the built_on list (or a mapping whose only key is built_on, so the block can be copied from an entry); [] means none.

index add clones the package (from --repo-dir or the URL) into a temporary directory, finds the receipts as committed at the pin or in an evidence-only descendant of it (untracked files do not count), checks out the pin, and runs the same validators as gate and comparator. It refuses a second entry for the same repository and commit.

An entry that already exists is refused unless --replace is given: that is how a package is re-pinned at a new gated commit. --replace writes the new entry over the old one, replaces its receipt copies, and carries the old entry’s built_on over unchanged unless --built-on-file is given, so a re-pin never drops the credits. The headlines, field tags and notes come from the flags as usual. The pull request shows the diff.

By default index add also fetches the public repository’s branches and refuses a pin or an evidence commit that no public branch contains, so an entry never points at history that only exists on one machine. --allow-unpushed skips that check for a provisional entry (the output says so); index check --clone refuses such an entry until the commits are pushed. Receipt copies are public: a receipt whose strings look like a local path is refused, and the comparator runner records COMPARATOR_RECEIPT_HOST_LABEL instead of the host name when that variable is set.

A Palomar registration grades an entry only when its commit equals the pin: index add keeps only those rows, and index check fetches each Palomar entry and compares its source.commit and source.repository_url with the entry.

Checking entries

lean-pkg index check                     # static: schema, copies, trust, duplicates
lean-pkg index check --clone             # every entry, re-derived from bytes at the pin
lean-pkg index check --clone my-lean --json

With --clone (or --repo-dir for one entry) the check re-derives the receipts and logs at the pin, compares the index copies byte for byte, checks the toolchain, lake-manifest.json, the license, the tag and the headline files, and recomputes trust. Palomar ids and the Reservoir listing are verified by API when the network is reachable; otherwise they are reported as skipped, never as failed or passed. Exit 0 when every entry passes, 1 on any failure, 2 on a usage error.

Docs-only descendants

The tag, and the commits the receipts are committed in, are bound by the same rule as gate, publish and comparator: an evidence-only descendant of the pin, or, when the package’s registry record opts in (docs_descendants: true, set with lean-pkg update NAME --accept-docs-descendants --reason R), a docs-only descendant: one where no build input changed (see Receipts). index add and index check --clone / --repo-dir read the opt-in from the registry they resolve (--registry, $LEAN_PKG_REGISTRY or the user default), and only from the record with the entry’s name and repository, never from a file in the package repository. Without a registry, or without the opt-in, the evidence-only rule binds; a tag the docs-only rule would admit is then refused with a clause that names the opt-in.

A repository whose HEAD has moved past the pin still passes: the pin is the claim. The rendered table shows the pin, not HEAD.

The static check refuses only a stated trust above the evidence; a stated trust below it is caught by --clone or --repo-dir, which recompute trust from bytes and require equality.

An unfinished project as an entry

A project does not have to be finished to be listed; it has to be honest. The index lists what is proved at a pin, nothing more, and the tool enforces that: the headline theorems must exist in the files named, their receipts must validate at the pin, and comparator trust requires every headline to be judged. An unfinished project is listed like this:

The lab’s own example is total-coloring-lean: a 700-theorem, sorry-free library whose README states that it proves an auxiliary edge-coloring theorem and a Δ+3 total assignment, and does not prove Vizing’s theorem or the conjecture. Its entry says exactly that. Its second pin added comparator evidence for both headline theorems, with Mathlib-only Challenge statements in the package’s Audit/ directory.

Pull requests

A contributor adds index/<name>/ and the rendered index/README.md in one pull request; the maintainer runs lean-pkg index check --clone <name> before merging and pastes the output into the review. Hosted CI runs the same check once the repository is public.

Next: Receipts and trust.