Companion to DESIGN.md, and written for the people building imprimatur. DESIGN.md says what to build; this file says in what order, and how we will know each part is right. Section references like “D§10.2” point into DESIGN.md.
docs/TESTING.md keeps a traceability matrix from each design section
(D§…) to the tests that cover it. Lean has no coverage tool, so this
matrix stands in for coverage. A pull request that changes behaviour
updates the matrix.UPDATE_GOLDEN=1, with the diff reviewed in
the pull request).sorry deep in a dependency
cone, disallowed axiom, missing key, anonymity leak) has a fixture that
triggers it and a test that the message and exit code are right.| Layer | What it covers | How it runs | Speed |
|---|---|---|---|
| Unit | pure functions: the TeX scanner and parser, balanced-brace extraction, checksum normalisation, slot extraction and merging, escaping, the Doc emitter (precedence, widths, flattening), canonical serialisation for hashing, TOML config, JSON reading and writing of the bundle |
lake test in each package |
seconds |
| Property | invariants over generated inputs (§2.3) | same, using a small seeded generator | seconds |
| Golden: extractor | every view of every declaration in the fixture projects (§2.2) | lake test in extract/, once per toolchain |
about a minute per toolchain |
| Golden: splicer | pairs of TeX files before and after apply, check reports, strip output |
lake test in splice/ |
seconds |
| Trust (negative) | each trust failure (§1, principle 5) on purpose-built fixtures | runs with the extractor golden tests | about a minute |
| End-to-end | the imprimatur build command line on the example projects in all three modes, then latexmk with pdflatex and lualatex: no LaTeX errors, and pdftotext output matches golden text |
scripts/e2e.sh, in CI |
a few minutes |
| Cross-toolchain | the same fixture gives byte-identical bundles, apart from the producer field, and identical stmtHash values, on every supported toolchain |
CI matrix job comparing bundles | a few minutes |
| Real-world integration | llmbda (parity, §4 M5), PLanet and the math catalogue, all Mathlib-based | scripts/integration.sh, run locally and before releases, not in CI (§2.5) |
tens of minutes |
The fixtures are small Lean projects under test/fixtures/, with no
Mathlib, so CI can build them on every toolchain in seconds. Each targets
part of the design:
| Fixture | Contents | Covers |
|---|---|---|
Basic |
theorems with implicit, instance and explicit binders; definitions; a structure; a docstring on every kind | the lean, meta, math and prose views; keys; entries |
Semantics |
a small STLC with an inductive typing relation and a small-step relation; value predicates; well-formedness side conditions; docstring labels /-- T-App: … -/ |
the rules and grammar views, rule labels, premise conventions, include/exclude, slots |
Notation |
constants used in every kind of notation rule: infix, nested pattern, hide, variant, flatten, width, prec |
the notation language (D§7.5) |
Trust |
sorry directly in a proof, and three levels deep in the cone; a custom axiom; partial and unsafe definitions; a theorem whose hypothesis definition exists in two versions (Weak := True, Strong := …), switched by a build option |
D§7.7, and the drift tests of D§10.3 |
ModuleSys |
files with module headers, private proofs, and import with and without all |
the private-level import (D§4, constraint 7) on the toolchains that have the module system |
Manifests |
a comparator-style ChallengeX.lean plus a JSON manifest; a mini blueprint .tex using \lean{} and \leanok |
D§10.5, D§9.3 |
The TeX fixtures live under test/tex/. Each is a small document exercising
one splicer behaviour:
\input, and \include;verbatim blocks containing fake markers;The splicer is where a bug corrupts authors’ files, so it gets the most
property tests. A small seeded generator (§2.4) produces TeX documents with
random prose, braces, comments, verbatim, blocks and slots, and random
bundles.
| Property | Statement |
|---|---|
| Locality | apply never changes a byte outside a block’s generated region and its sum= option. This is checked by masking the blocks and comparing. |
| Idempotence | apply(apply(d, b), b) = apply(d, b). |
| Fixed point | check(apply(d, b), b) reports nothing stale. |
| Slot preservation | for every slot id present both before and after, the slot’s text after apply equals its text before. |
| Edit detection | for any single-character edit inside a generated region, outside slots, check reports a hand edit; inside a slot, it doesn’t. |
| Normalisation | converting a document to CRLF, or adding trailing whitespace, doesn’t change any checksum’s verdict. |
| Strip | after strip, the output contains no imprimatur markers, and contains every generated region verbatim. |
| Scanner robustness | on any input, including truncated files, unbalanced braces and markers inside verbatim, scan either succeeds or reports an error with a position. It never crashes, and never writes a file. |
| Hash invariance | in the extractor, renaming bound variables or universe parameters doesn’t change stmtHash; changing a hypothesis does. |
check,
checkEq, golden comparison with UPDATE_GOLDEN, and a seeded generator
that reproduces failures from a printed seed.
RunLatex/Test.lean harness is the model.UPDATE_GOLDEN=1 and shows up as a reviewable diff.scripts/test-all.sh runs every layer that CI runs, so a contributor
can reproduce CI locally with a single command.| Job | Matrix | Contents |
|---|---|---|
splice |
one toolchain | build with warnings as errors; unit, property and golden tests |
extract |
v4.28.0-rc1, v4.31.0, v4.34.1 (the three motivating projects), plus the latest stable | build the fixtures; unit, golden and trust tests |
cross-toolchain |
needs extract |
compare bundles and stmtHash values across the matrix |
e2e |
one toolchain, with TeX Live (pdflatex and lualatex) |
scripts/e2e.sh on examples/ in all three modes |
lint |
— | markdown links, JSON schema validation of golden bundles, the traceability matrix has no orphan entries |
Not in CI: Mathlib-based integration. A Mathlib cache costs about 5 GB
per toolchain, and private repositories on the free plan get 2,000 Actions
minutes a month. scripts/integration.sh runs it locally against the real
projects. It is required before every release, and its report is attached to
the release.
Branch rules: main is protected; every change arrives as a pull
request with green CI; releases are tags following semantic versioning, with
CHANGELOG.md entries.
Each spike ends with a short written result in docs/spikes/, and if
needed a change to DESIGN.md.
| # | Question | Done when | If it fails |
|---|---|---|---|
| S1 | External mode. Can a prebuilt extractor combine its own .olean files with a host’s lake env search path, elaborate a notation file in-process with the frontend, and then import the host modules at private level? This must work on v4.28.0-rc1, v4.31.0 and v4.34.1 |
a 100-line program does all of this against PLanet’s project on all three toolchains | sidecar mode becomes the default; D§6.3 is updated |
| S2 | Stable hashing. Does a canonical serialisation of Expr, with binder names dropped and universe parameters renamed, give the same hash for the same declaration on all three toolchains, and do the dependency-cone walk and collectAxioms behave the same way? |
the same hashes for the Trust fixture on three toolchains |
the hash is defined per toolchain, and check reports “toolchain changed, run accept” instead of drift |
| S3 | Parity baseline. How much of llmbda’s current output can a generic rules view reproduce? |
a list of llmbda’s rendering special cases, each marked as generic, notation, convention or custom view | the scope of the custom views for M5 is planned from this list |
S1 and S2 run in the first week, since external mode and hashing shape milestones M2 and M3.
Results.
latex_style, latex_entry, label
styles, alias templates and labels, and comment-delimited blocks.Each milestone ends with green CI, an updated traceability matrix, and a tag. “Tests first” means the listed tests are merged, failing, before the code that makes them pass.
Status: done on branch m0-foundations (2026-10-17), apart from green CI on
GitHub, which needs the branch pushed. §7’s decisions were taken at their
defaults:
the repository stays private until v0.5.0.
test/ and scripts/,
Apache headers, CONTRIBUTING.md, templates for pull requests and issues.autoImplicit false, all linters on, warnings as errors.docs/TESTING.md with an empty traceability matrix listing every D§
section.The splicer is pure text with no Lean internals, so it can be built completely, test-first, before the extractor exists. Its input is hand-written golden bundles.
check reports for each failure mode.\input, \include and \subfile, and
skipping comments and verbatim;scan, apply, check (with --diff), strip, migrate-slots;schema/bundle.schema.json;imprimatur.toml.paper.tex goes through scan and strip
without changing a byte outside its blocks.Basic, covering the lean and
meta views; trust fixtures for direct sorry and custom axioms; the
ModuleSys fixture; the cross-toolchain job.Compat/, at private level;lean view, with semantic macros, through the delaborator and
open_scoped;meta view;collectAxioms and sorry detection;imprimatur-export, and the imprimatur wrapper in sidecar and
in-project modes;relative as the default;imprimatur.sty, with the token macros.e2e job builds examples/minimal into a PDF in both
modes. Also, scripts/integration.sh runs the lean view over PLanet’s
Planet.Paper.* and over the theorem in the math repository’s
Separation.lean, with outputs reviewed by hand.Trust fixture, including Weak/Strong drift
and sorry three levels down; hash-invariance properties; the
Manifests fixture; \leancheck and accept round trips.trusted_prefixes;stmtHash and sigHash;\leancheck and accept;@challenge entries;check gives the right verdict on every Trust case on every
toolchain;Notation fixture with golden output for every
feature of a notation rule; unit tests of the Doc emitter (precedence
tables, widths, line breaks, flattening, escaping of every TeX special
character).Doc IR and emitter;latex_notation command and its environment extension;Expr with the delaborator fallback;variant, flatten, width, hide, prec;math and prose views;core, logic, sets, order), each tested against
the fixtures.prose view
to the agreed target text (D§3; reviewed by hand in the integration run),
and every pack rule has at least one golden use.Status: done on branch m5-rules (2026-10-18). The parity gate passes
byte for byte. llmbda’s notation module and custom views live in llmbda
(imprimatur/, on llmbda’s imprimatur branch), whose three documents are
now built with imprimatur in external mode; llmbda’s old exporter, and the
gate with it, are deleted there. PLanet’s rules
are generated (integration/planet-rules), with Lift hand-written. show=
and hide= are not implemented, and migrate-slots was not needed.
Semantics fixture golden files for rules and
grammar; premise conventions; include and exclude; label precedence;
slots in grammars; the parity harness.rules and grammar views;latex_metavar_convention and latex_hide_premise;rule, def, forall, names);@[latex_view].oopsla2027/paper.tex
with the old run_latex and with imprimatur from the same commit. It
passes only if every difference is a sum= addition. Only then is the old
code deleted from llmbda.\leanindex output; lint fixtures; anonymity
fixtures (an absolute path, a user name or a URL planted in each output
channel must be caught).\leanindex, lint, check --anonymous, undefined-macro
warnings, --blueprint-compat, release binaries for Linux, macOS and
Windows, the toolchain range documented and enforced.submission profile and passes both
check --anonymous and its own check-anonymity.sh. A release candidate
is used for a week on a real paper before v0.5.0 is tagged.docs/TESTING.md is updated, and DESIGN.md
is updated if behaviour differs from it.UPDATE_GOLDEN.CHANGELOG.md entry for anything a user would notice.| Risk | Likelihood | Mitigation |
|---|---|---|
| External mode is impossible on some toolchains | medium | spike S1 first; sidecar mode is a complete fallback |
Lean internals change between toolchains (delaborator, importModules, frontend) |
high, over time | everything version-specific lives in Compat/; CI covers the matrix; tags per toolchain if needed (D§13) |
| Golden files get approved without being read | medium | the definition of done; golden diffs kept small by giving each fixture one concern |
| llmbda parity takes longer than planned because of its special cases | medium | spike S3 measures it before M5 is planned |
| Mathlib integration is too heavy for CI and this machine (35 GB free disk) | high | Mathlib stays out of CI; integration runs locally, one toolchain at a time, reusing each project’s existing .lake |
| The private repository runs out of Actions minutes | low to medium | the extractor matrix runs on pull requests, and the full matrix nightly; or make the repository public before v0.5 |