imprimatur

Blocks and the splicer

For authors of papers that use imprimatur. This page describes the TeX markup and what imprimatur-splice does with it; views.md describes the generated content. DESIGN.md §9–§10 gives the reasoning behind it.

Setting up

Put imprimatur.toml next to the main .tex file:

schema = 1
main = "paper.tex"
lean_project = "lean"            # the package that requires imprimatur
mode = "in-project"              # or "sidecar", or "external"
imports = ["Minimal"]            # the modules declarations come from
strip_namespaces = ["Minimal"]

[aliases]
leantheorem = { view = "lean", wrap = "theorem" }

Then add \usepackage{imprimatur} to the paper (tex/imprimatur.sty), and for each alias \leanblockalias{leantheorem}{theorem}. Run imprimatur build after changing the Lean or the paper, and imprimatur check in CI.

The Lean project is reached in one of three ways:

In-project. The project’s own lakefile requires imprimatur (subDir = "extract").
Sidecar. A small package next to the project requires both the project and imprimatur, so the project itself doesn’t change.
External. Nothing requires imprimatur. Run imprimatur toolchain install VERSION once for the project’s toolchain; imprimatur build then reads the project, which must already be built, without changing it.

examples/minimal, examples/sidecar and examples/external show all three. examples/semantics is a short paper on a typed λ-calculus with name-carrying terms, in external mode, that shows the two ways of tying a paper to Lean side by side: a generated grammar (with the authors’ descriptions kept as slots), swapping and α-equivalence in the style of Pitts’s nominal techniques, generated typing and reduction rules, and generated results up to preservation and progress, next to hand-written statements checked with \leancheck. Each example’s paper.tex is the input, with its blocks empty; expected/paper.tex is the paper imprimatur makes from it, and both compile in an editor (their .latexmkrc puts tex/ on the path).

Markup

Form	Example	What the splicer does
block	`\begin{leanblock}[view=math]{Key}{Title}` … `\end{leanblock}`	regenerates the content between the header and `\end`
inline	`\leaninline{Key}{}`	regenerates the second argument
reference	`\leanref{Key}{}`	fills the second argument with the source location, per profile
check	`\leancheck{Key1, Key2}`	generates nothing; `check` reports missing keys and untrusted results
hypothesis reference	`\leanhypref{Key}{h}`	prints `(h)`, and makes the prose view of `Key` label its hypothesis `h`
index	`\leanindex`	recognised; generated from M6
slot	`\leanslot{id}{text}`	inside generated content: text that belongs to the authors

Write new inline items and references with an empty second argument, as in \leaninline{Key}{}. The splicer fills it in. The second argument is always present, so the macros take a fixed number of arguments in TeX.

Aliases. Environments listed under [aliases] in imprimatur.toml work like leanblock, with a fixed view. They take the same {Key}{Title} arguments, so a paper can keep its existing environment names:

[aliases]
leantheorem = { view = "math", wrap = "theorem" }
leangrammar = { view = "grammar", slots = { macros = ["\\entry"], arg = 2, id = "arg1" } }

An alias can also shape what is written into its blocks:

leanlemma  = { view = "prose", wrap = "lemma", label = "lem:{key}", repeat_suffix = "-appendix",
               template = "\\label\n\n{content}" }
leandef    = { view = "math", label = "def:{key}", template = "\\label\n\\({content}\\)" }
LEANCLAUSE = { view = "math", comment = true, template = "\\clause<h1 id="testing-imprimatur">Testing imprimatur</h1>

<p><em>For contributors. <a href="/imprimatur/PLAN.html">PLAN.md</a> §2 describes the test layers; this
file says how to run them and keeps the traceability matrix.</em></p>

<h2 id="running-the-tests">Running the tests</h2>

<table>
  <thead>
    <tr>
      <th>What</th>
      <th>Command</th>
      <th>Where</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>everything CI runs</td>
      <td><code class="language-plaintext highlighter-rouge">scripts/test-all.sh</code></td>
      <td>repository root</td>
    </tr>
    <tr>
      <td>integration with the real projects (not in CI)</td>
      <td><code class="language-plaintext highlighter-rouge">scripts/integration.sh</code></td>
      <td>repository root</td>
    </tr>
    <tr>
      <td>the test harness’s own tests</td>
      <td><code class="language-plaintext highlighter-rouge">lake test</code></td>
      <td><code class="language-plaintext highlighter-rouge">testkit/</code></td>
    </tr>
    <tr>
      <td>extractor tests (build the fixtures first)</td>
      <td><code class="language-plaintext highlighter-rouge">lake test</code></td>
      <td><code class="language-plaintext highlighter-rouge">extract/test/</code></td>
    </tr>
    <tr>
      <td>end-to-end examples (needs TeX Live)</td>
      <td><code class="language-plaintext highlighter-rouge">scripts/e2e.sh</code></td>
      <td>repository root</td>
    </tr>
    <tr>
      <td>splicer tests</td>
      <td><code class="language-plaintext highlighter-rouge">lake test</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/test/</code></td>
    </tr>
    <tr>
      <td>the extractor on another toolchain</td>
      <td><code class="language-plaintext highlighter-rouge">scripts/test-all.sh --toolchain v4.31.0</code></td>
      <td>repository root</td>
    </tr>
    <tr>
      <td>lint (links, schema, this matrix)</td>
      <td><code class="language-plaintext highlighter-rouge">scripts/lint.sh</code></td>
      <td>repository root</td>
    </tr>
  </tbody>
</table>

<p>Each test package is a separate Lake package that requires the package it
tests and <code class="language-plaintext highlighter-rouge">testkit/</code>. The shipped packages therefore never depend on test
code (PLAN §1.6). A test package has no <code class="language-plaintext highlighter-rouge">lean-toolchain</code> of its own; <code class="language-plaintext highlighter-rouge">elan</code>
finds the one in the package it tests.</p>

<p><strong>Environment variables.</strong></p>

<ul>
  <li><code class="language-plaintext highlighter-rouge">UPDATE_GOLDEN=1</code> rewrites golden files instead of comparing them. Review
the resulting diff line by line before committing it (PLAN §5).</li>
  <li><code class="language-plaintext highlighter-rouge">IMPRIMATUR_CASES=n</code> sets the number of cases per property (default 100;
M1’s gate is 10,000).</li>
  <li><code class="language-plaintext highlighter-rouge">IMPRIMATUR_SEED=s</code> fixes the base seed. A failing property prints the
seed and case count that reproduce it.</li>
  <li><code class="language-plaintext highlighter-rouge">IMPRIMATUR_MAX_SIZE=n</code> bounds the size of generated values (default 30).</li>
</ul>

<p><strong>Builds</strong> use <code class="language-plaintext highlighter-rouge">lake build --wfail</code> in CI and in <code class="language-plaintext highlighter-rouge">scripts/test-all.sh</code>. The
lakefiles don’t make warnings errors, so that a user on a newer toolchain
isn’t broken by a new deprecation warning.</p>

<h2 id="test-names">Test names</h2>

<p>Every check has a name of the form <code class="language-plaintext highlighter-rouge">package/area/what</code>, for example
<code class="language-plaintext highlighter-rouge">splice/prop/idempotence</code>. The matrix below refers to tests by these names,
and <code class="language-plaintext highlighter-rouge">scripts/check-traceability.py</code> checks that every name in it appears as a
string literal in a test source. Checks done by scripts are named
<code class="language-plaintext highlighter-rouge">lint/…</code> (in <code class="language-plaintext highlighter-rouge">scripts/</code>), <code class="language-plaintext highlighter-rouge">integration/…</code> (in <code class="language-plaintext highlighter-rouge">scripts/integration.sh</code>) or
<code class="language-plaintext highlighter-rouge">e2e/…</code> (in <code class="language-plaintext highlighter-rouge">scripts/e2e.sh</code>).</p>

<p><strong>Golden bundles of the extractor.</strong> <code class="language-plaintext highlighter-rouge">extract/test/golden/&lt;fixture&gt;.bundle.json</code>
holds the bundle of each fixture under <code class="language-plaintext highlighter-rouge">test/fixtures/</code>, with the toolchain in
<code class="language-plaintext highlighter-rouge">producer.lean</code> masked as <code class="language-plaintext highlighter-rouge">v4.x</code>. The same golden files must hold on every
toolchain in the CI matrix.</p>

<p><strong>Golden tests of the splicer.</strong> Each directory under <code class="language-plaintext highlighter-rouge">test/tex/</code> is a case:
a document, its configuration and bundles, and a <code class="language-plaintext highlighter-rouge">steps</code> file of commands.
The test runs the steps and compares a transcript with
<code class="language-plaintext highlighter-rouge">splice/test/golden/&lt;case&gt;.txt</code> (see <code class="language-plaintext highlighter-rouge">splice/test/SpliceTest/Golden.lean</code>).</p>

<h2 id="traceability-matrix">Traceability matrix</h2>

<p>Lean has no coverage tool, so this matrix stands in for coverage (PLAN §1.1).
There is one row per requirement, and every numbered section of
<a href="/imprimatur/DESIGN.html">DESIGN.md</a> has at least one row. <strong>Tests</strong> lists test names,
or <code class="language-plaintext highlighter-rouge">—</code> if there are none yet. <strong>When</strong> is the milestone that brings the tests
(PLAN §4), or <code class="language-plaintext highlighter-rouge">n/a</code> for sections that describe no behaviour.</p>

<p><code class="language-plaintext highlighter-rouge">scripts/check-traceability.py</code> (run by <code class="language-plaintext highlighter-rouge">scripts/lint.sh</code> and the <code class="language-plaintext highlighter-rouge">lint</code> CI
job) fails if a section of DESIGN.md has no row, a row names a section that
doesn’t exist, or a row names a test that doesn’t exist.</p>

<table>
  <thead>
    <tr>
      <th>Section</th>
      <th>Requirement</th>
      <th>Tests</th>
      <th>When</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>D§1</td>
      <td>goals and non-goals</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§2</td>
      <td>motivating projects</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§3</td>
      <td>prior art</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(1) the extractor builds and runs on every supported toolchain</td>
      <td><code class="language-plaintext highlighter-rouge">extract/version/lean</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Basic</code></td>
      <td>M0</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(2) the splicer imports nothing from Lean but <code class="language-plaintext highlighter-rouge">Lean.Data.Json</code></td>
      <td><code class="language-plaintext highlighter-rouge">lint/splice-imports</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(3) a notation rule naming a missing constant fails at build time (checked when the <code class="language-plaintext highlighter-rouge">Notation</code> fixture builds; the messages are tested by hand)</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(4) every declaration has a default rendering (the <code class="language-plaintext highlighter-rouge">lean</code> view)</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">integration/planet-lean-view</code>, <code class="language-plaintext highlighter-rouge">integration/math-lean-view</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(5) external mode changes nothing in the host project</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/external</code>, <code class="language-plaintext highlighter-rouge">e2e/semantics</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(6) shipped packages have no Lake dependencies</td>
      <td><code class="language-plaintext highlighter-rouge">lint/no-deps</code></td>
      <td>M0 (lint)</td>
    </tr>
    <tr>
      <td>D§4</td>
      <td>(7) environments are imported at <code class="language-plaintext highlighter-rouge">private</code> level</td>
      <td><code class="language-plaintext highlighter-rouge">extract/modules/private-sorry-seen</code>, <code class="language-plaintext highlighter-rouge">extract/modules/sorry-through-import-all</code>, <code class="language-plaintext highlighter-rouge">extract/golden/ModuleSys</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§5</td>
      <td>extractor and splicer communicate only through the bundle</td>
      <td><code class="language-plaintext highlighter-rouge">splice/version/schema</code>, <code class="language-plaintext highlighter-rouge">extract/version/schema</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§5</td>
      <td><code class="language-plaintext highlighter-rouge">imprimatur build</code> runs scan, export, apply; <code class="language-plaintext highlighter-rouge">check</code> passes after it</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/minimal</code>, <code class="language-plaintext highlighter-rouge">e2e/sidecar</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§6.1</td>
      <td><code class="language-plaintext highlighter-rouge">imprimatur.toml</code> is parsed; unknown keys and bad values are reported</td>
      <td><code class="language-plaintext highlighter-rouge">splice/toml/parses</code>, <code class="language-plaintext highlighter-rouge">splice/toml/duplicate-key</code>, <code class="language-plaintext highlighter-rouge">splice/toml/error-line</code>, <code class="language-plaintext highlighter-rouge">splice/config/parses</code>, <code class="language-plaintext highlighter-rouge">splice/config/unknown-key</code>, <code class="language-plaintext highlighter-rouge">splice/config/alias-needs-view</code>, <code class="language-plaintext highlighter-rouge">splice/config/url-needs-template</code>, <code class="language-plaintext highlighter-rouge">splice/golden/config-errors</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§6.2</td>
      <td>the notation module is elaborated and its names resolved, in-project and as a file in external mode</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code>, <code class="language-plaintext highlighter-rouge">e2e/minimal</code>, <code class="language-plaintext highlighter-rouge">e2e/external</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§6.3</td>
      <td>sidecar and in-project modes</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/minimal</code>, <code class="language-plaintext highlighter-rouge">e2e/sidecar</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§6.3</td>
      <td>external mode, with <code class="language-plaintext highlighter-rouge">imprimatur toolchain install</code></td>
      <td><code class="language-plaintext highlighter-rouge">e2e/external</code>, <code class="language-plaintext highlighter-rouge">integration/math-manifests</code>, <code class="language-plaintext highlighter-rouge">integration/planet-drift</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§7.1</td>
      <td><code class="language-plaintext highlighter-rouge">Doc</code> emitter: escaping, parenthesisation, line breaking</td>
      <td><code class="language-plaintext highlighter-rouge">extract/doc/escape-specials</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-symbols</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-wrappers</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-spacing</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-scripts</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-given</code>, <code class="language-plaintext highlighter-rouge">extract/doc/no-parens-left-assoc</code>, <code class="language-plaintext highlighter-rouge">extract/doc/parens-right</code>, <code class="language-plaintext highlighter-rouge">extract/doc/parens-tighter</code>, <code class="language-plaintext highlighter-rouge">extract/doc/no-parens-looser</code>, <code class="language-plaintext highlighter-rouge">extract/doc/width-counts-parens</code>, <code class="language-plaintext highlighter-rouge">extract/doc/fits-unbroken</code>, <code class="language-plaintext highlighter-rouge">extract/doc/breaks-outermost</code>, <code class="language-plaintext highlighter-rouge">extract/doc/breaks-deeper-when-needed</code>, <code class="language-plaintext highlighter-rouge">extract/doc/break-after-control-space</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.2</td>
      <td>notation matches <code class="language-plaintext highlighter-rouge">Expr</code>; unmatched subterms are rendered as functions, or delaborated</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code>, <code class="language-plaintext highlighter-rouge">extract/notation/no-render-errors</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td><code class="language-plaintext highlighter-rouge">lean</code> view, with semantic token macros</td>
      <td><code class="language-plaintext highlighter-rouge">extract/tokens/line</code>, <code class="language-plaintext highlighter-rouge">extract/tokens/subscripts-and-primes</code>, <code class="language-plaintext highlighter-rouge">extract/names/strip</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">integration/planet-lean-view</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td><code class="language-plaintext highlighter-rouge">meta</code> view; the splicer fills its source location per profile</td>
      <td><code class="language-plaintext highlighter-rouge">extract/markdown/code</code>, <code class="language-plaintext highlighter-rouge">extract/markdown/maths</code>, <code class="language-plaintext highlighter-rouge">extract/markdown/unbalanced-maths</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">splice/golden/meta-source</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td><code class="language-plaintext highlighter-rouge">prose</code> labels only hypotheses the paper refers to (<code class="language-plaintext highlighter-rouge">\leanhypref</code>)</td>
      <td><code class="language-plaintext highlighter-rouge">extract/prose/hyp-referred-labelled</code>, <code class="language-plaintext highlighter-rouge">extract/prose/hyp-unreferred-unlabelled</code>, <code class="language-plaintext highlighter-rouge">splice/golden/hyprefs</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td><code class="language-plaintext highlighter-rouge">math</code> and <code class="language-plaintext highlighter-rouge">prose</code> views</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code>, <code class="language-plaintext highlighter-rouge">e2e/minimal</code>, <code class="language-plaintext highlighter-rouge">e2e/fixture-views</code>, <code class="language-plaintext highlighter-rouge">integration/math-prose</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td><code class="language-plaintext highlighter-rouge">rules</code> and <code class="language-plaintext highlighter-rouge">grammar</code> views</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, <code class="language-plaintext highlighter-rouge">e2e/fixture-views</code>, <code class="language-plaintext highlighter-rouge">e2e/semantics</code>, <code class="language-plaintext highlighter-rouge">integration/planet-rules</code>, llmbda’s parity gate</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.3</td>
      <td>custom views through <code class="language-plaintext highlighter-rouge">@[latex_view]</code>, with the document inventory</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code> (<code class="language-plaintext highlighter-rouge">fixture.rulelist</code>), llmbda’s parity gate (four custom views)</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.4</td>
      <td>rule label precedence; <code class="language-plaintext highlighter-rouge">latex_rules</code> templates, anchors, <code class="language-plaintext highlighter-rouge">sep</code>, <code class="language-plaintext highlighter-rouge">doc_labels</code>; groups across inductives</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, llmbda’s parity gate</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.5</td>
      <td>notation rules: patterns, templates, <code class="language-plaintext highlighter-rouge">prec</code>, <code class="language-plaintext highlighter-rouge">width</code>, <code class="language-plaintext highlighter-rouge">hide</code>, <code class="language-plaintext highlighter-rouge">variant</code>, <code class="language-plaintext highlighter-rouge">flatten</code>, typed patterns, lookup order, metavariables</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code>, <code class="language-plaintext highlighter-rouge">extract/doc/template-prime</code>, <code class="language-plaintext highlighter-rouge">extract/doc/template-longest</code>, <code class="language-plaintext highlighter-rouge">extract/doc/template-unknown</code>, <code class="language-plaintext highlighter-rouge">extract/doc/metavar-subscript</code>, <code class="language-plaintext highlighter-rouge">extract/doc/metavar-digits</code>, <code class="language-plaintext highlighter-rouge">extract/doc/metavar-prime</code>, <code class="language-plaintext highlighter-rouge">extract/doc/metavar-long</code>, <code class="language-plaintext highlighter-rouge">extract/doc/metavar-renamed</code>, <code class="language-plaintext highlighter-rouge">splice/golden/notation-config</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.5</td>
      <td>packs: every rule has a golden use, and the output typesets with both engines</td>
      <td><code class="language-plaintext highlighter-rouge">extract/notation/every-pack-rule-used</code>, <code class="language-plaintext highlighter-rouge">e2e/fixture-views</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.5</td>
      <td>the bundle records the macros each rendering uses</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code></td>
      <td>M4</td>
    </tr>
    <tr>
      <td>D§7.5</td>
      <td>binder patterns, partial applications, <code class="language-plaintext highlighter-rouge">flatten</code> with <code class="language-plaintext highlighter-rouge">sep</code>, <code class="language-plaintext highlighter-rouge">assoc</code>, <code class="language-plaintext highlighter-rouge">latex_style</code>, <code class="language-plaintext highlighter-rouge">latex_entry</code>, Greek letters, several notation files</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code> (<code class="language-plaintext highlighter-rouge">math:binders</code>), <code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, llmbda’s parity gate</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§18.2</td>
      <td>the splicer’s laws and Theorem 1, proved for a model of the splicer; the paper presenting them is built and checked with no warnings</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/about</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§18.4</td>
      <td>translation validation: tokens, productions of rules, readings counted up to two, sorts and type variables, coercions, chains, the built-in forms</td>
      <td><code class="language-plaintext highlighter-rouge">extract/validate/tokens</code>, <code class="language-plaintext highlighter-rouge">extract/validate/tokens-code</code>, <code class="language-plaintext highlighter-rouge">extract/validate/production</code>, <code class="language-plaintext highlighter-rouge">extract/validate/production-atomic</code>, <code class="language-plaintext highlighter-rouge">extract/validate/production-coercion</code>, <code class="language-plaintext highlighter-rouge">extract/validate/ambiguous</code>, <code class="language-plaintext highlighter-rouge">extract/validate/no-reading-without-parens</code>, <code class="language-plaintext highlighter-rouge">extract/validate/one-reading-with-parens</code>, <code class="language-plaintext highlighter-rouge">extract/validate/assoc-left</code>, <code class="language-plaintext highlighter-rouge">extract/validate/assoc-none</code>, <code class="language-plaintext highlighter-rouge">extract/validate/sorts</code>, <code class="language-plaintext highlighter-rouge">extract/validate/coercion-one-reading</code>, <code class="language-plaintext highlighter-rouge">extract/validate/flatten</code>, <code class="language-plaintext highlighter-rouge">extract/validate/builtin-implies</code>, <code class="language-plaintext highlighter-rouge">extract/validate/builtin-forall</code>, <code class="language-plaintext highlighter-rouge">extract/validate/tyvar-ill-sorted</code>, <code class="language-plaintext highlighter-rouge">extract/validate/tyvar-unknown</code>, <code class="language-plaintext highlighter-rouge">extract/validate/tyvar-binds</code>, <code class="language-plaintext highlighter-rouge">extract/validate/sort-arrow</code>, <code class="language-plaintext highlighter-rouge">extract/validate/sort-arrow-differs</code>, <code class="language-plaintext highlighter-rouge">extract/validate/sort-args-differ</code>, <code class="language-plaintext highlighter-rouge">extract/validate/sort-args-open</code>, <code class="language-plaintext highlighter-rouge">extract/validate/coercion-sorts</code>, <code class="language-plaintext highlighter-rouge">extract/validate/coercion-sorts-needed</code>, <code class="language-plaintext highlighter-rouge">extract/validate/application-curried</code>, <code class="language-plaintext highlighter-rouge">extract/validate/synonym</code>, <code class="language-plaintext highlighter-rouge">extract/validate/unmodelled</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§18.3</td>
      <td>side condition 5: a variable that prints as another type’s category letter is reported</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code> (<code class="language-plaintext highlighter-rouge">Stlc.size_pos</code>), <code class="language-plaintext highlighter-rouge">e2e/about</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§18.4</td>
      <td>the bundle records each view’s problems; <code class="language-plaintext highlighter-rouge">check</code> warns at typeset blocks only, for the view they show</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Notation</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, <code class="language-plaintext highlighter-rouge">splice/golden/validation</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§18.4</td>
      <td>a template that drops a pattern variable is a warning</td>
      <td>the <code class="language-plaintext highlighter-rouge">#guard_msgs</code> test in <code class="language-plaintext highlighter-rouge">extract/test/ExtractTest/Validate.lean</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.6</td>
      <td>premise conventions</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, <code class="language-plaintext highlighter-rouge">e2e/fixture-views</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§7.7</td>
      <td>axioms and <code class="language-plaintext highlighter-rouge">sorry</code></td>
      <td><code class="language-plaintext highlighter-rouge">extract/trust/direct-sorry</code>, <code class="language-plaintext highlighter-rouge">extract/trust/custom-axiom</code>, <code class="language-plaintext highlighter-rouge">extract/trust/classical-axioms</code>, <code class="language-plaintext highlighter-rouge">extract/trust/sorry-in-proof-chain</code>, <code class="language-plaintext highlighter-rouge">extract/trust/sorry-in-statement</code>, <code class="language-plaintext highlighter-rouge">extract/trust/custom-axiom-trust</code>, <code class="language-plaintext highlighter-rouge">extract/modules/private-sorry-seen</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§7.7</td>
      <td>dependency cone up to <code class="language-plaintext highlighter-rouge">trusted_prefixes</code>, with reasons</td>
      <td><code class="language-plaintext highlighter-rouge">extract/trust/cone-sorry</code>, <code class="language-plaintext highlighter-rouge">extract/trust/cone-partial</code>, <code class="language-plaintext highlighter-rouge">extract/trust/cone-clean</code>, <code class="language-plaintext highlighter-rouge">splice/golden/cone</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§7.7</td>
      <td><code class="language-plaintext highlighter-rouge">stmtHash</code>: insensitive to binder and universe names, sensitive to meaning, stable across toolchains</td>
      <td><code class="language-plaintext highlighter-rouge">extract/prop/hash-binder-names</code>, <code class="language-plaintext highlighter-rouge">extract/prop/hash-universe-names</code>, <code class="language-plaintext highlighter-rouge">extract/prop/hash-sees-constants</code>, <code class="language-plaintext highlighter-rouge">extract/prop/hash-ignores-mdata</code>, <code class="language-plaintext highlighter-rouge">extract/hash/sorry-tag-ignored</code>, <code class="language-plaintext highlighter-rouge">extract/hash/binder-kind-matters</code>, <code class="language-plaintext highlighter-rouge">extract/trust/same-hash-renamed-binder</code>, <code class="language-plaintext highlighter-rouge">extract/trust/same-hash-renamed-universes</code>, <code class="language-plaintext highlighter-rouge">extract/trust/weakened-hypothesis-drifts</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Trust</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§7.7</td>
      <td><code class="language-plaintext highlighter-rouge">sigHash</code> change alone is a warning</td>
      <td><code class="language-plaintext highlighter-rouge">extract/trust/weakened-hypothesis-same-signature</code>, <code class="language-plaintext highlighter-rouge">extract/trust/different-sig-renamed</code>, <code class="language-plaintext highlighter-rouge">splice/golden/drift</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§8</td>
      <td>bundles are deterministic: sorted keys, no timestamps; the same on every toolchain</td>
      <td><code class="language-plaintext highlighter-rouge">extract/json/sorted</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">extract/golden/ModuleSys</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Trust</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§8</td>
      <td>bundles contain no absolute paths, user names, URLs or commit hashes</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">splice/bundle/absolute-path</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§8</td>
      <td>bundles are read and checked against the rules of <code class="language-plaintext highlighter-rouge">schema/bundle.schema.json</code>; golden bundles validate against the schema</td>
      <td><code class="language-plaintext highlighter-rouge">splice/bundle/parses</code>, <code class="language-plaintext highlighter-rouge">splice/bundle/schema-version</code>, <code class="language-plaintext highlighter-rouge">splice/bundle/absolute-path</code>, <code class="language-plaintext highlighter-rouge">splice/bundle/missing-views</code>, <code class="language-plaintext highlighter-rouge">splice/golden/bundle-errors</code>, <code class="language-plaintext highlighter-rouge">lint/bundle-schema</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§8</td>
      <td>a view that fails to render is recorded in <code class="language-plaintext highlighter-rouge">errors</code>, and is an error only if requested</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">splice/golden/failures</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§9.1</td>
      <td><code class="language-plaintext highlighter-rouge">leanblock</code>, <code class="language-plaintext highlighter-rouge">\leaninline</code>, <code class="language-plaintext highlighter-rouge">\leanref</code>, <code class="language-plaintext highlighter-rouge">\leancheck</code>, <code class="language-plaintext highlighter-rouge">\leanindex</code> are recognised</td>
      <td><code class="language-plaintext highlighter-rouge">splice/scan/forms</code>, <code class="language-plaintext highlighter-rouge">splice/scan/options</code>, <code class="language-plaintext highlighter-rouge">splice/scan/check-keys</code>, <code class="language-plaintext highlighter-rouge">splice/golden/basic</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§9.1</td>
      <td>block options: <code class="language-plaintext highlighter-rouge">include</code>/<code class="language-plaintext highlighter-rouge">exclude</code> and the theorem modifiers (<code class="language-plaintext highlighter-rouge">show</code>/<code class="language-plaintext highlighter-rouge">hide</code> are not implemented)</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Semantics</code>, <code class="language-plaintext highlighter-rouge">splice/golden/basic</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§9.2</td>
      <td>alias options <code class="language-plaintext highlighter-rouge">label</code>, <code class="language-plaintext highlighter-rouge">repeat_suffix</code>, <code class="language-plaintext highlighter-rouge">template</code>, <code class="language-plaintext highlighter-rouge">comment</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/aliases</code>, llmbda’s parity gate</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§10.1</td>
      <td>definitions of imprimatur’s macros are not uses</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/definitions</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§10.1</td>
      <td>conditionals: blocks in branches that are off (<code class="language-plaintext highlighter-rouge">\iffalse</code>, <code class="language-plaintext highlighter-rouge">\newif</code> switches) are maintained but not typeset; the document inventory</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/conditionals</code>, <code class="language-plaintext highlighter-rouge">splice/golden/aliases</code>, llmbda’s parity gate</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§9.2</td>
      <td>aliases map existing environments onto <code class="language-plaintext highlighter-rouge">leanblock</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/config/alias-slots</code>, <code class="language-plaintext highlighter-rouge">splice/golden/basic</code>, <code class="language-plaintext highlighter-rouge">splice/golden/positional-slots</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§9.3</td>
      <td>blueprint <code class="language-plaintext highlighter-rouge">\lean{…}</code> read as check-only references; <code class="language-plaintext highlighter-rouge">\leanok</code> cross-checked</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/blueprint</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§9.3</td>
      <td><code class="language-plaintext highlighter-rouge">--blueprint-compat</code> writes <code class="language-plaintext highlighter-rouge">\lean{…}</code></td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§9.4</td>
      <td>a document compiles with <code class="language-plaintext highlighter-rouge">imprimatur.sty</code> (pdflatex and lualatex) and shows the spliced content</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/minimal</code>, <code class="language-plaintext highlighter-rouge">e2e/sidecar</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§9.5</td>
      <td>slots keep their text by id; slot edits are not hand edits</td>
      <td><code class="language-plaintext highlighter-rouge">e2e/semantics</code>, <code class="language-plaintext highlighter-rouge">splice/slots/merge</code>, <code class="language-plaintext highlighter-rouge">splice/checksum/ignores-slot-text</code>, <code class="language-plaintext highlighter-rouge">splice/prop/slot-preservation</code>, <code class="language-plaintext highlighter-rouge">splice/prop/edit-detection</code>, <code class="language-plaintext highlighter-rouge">splice/golden/slots</code>, <code class="language-plaintext highlighter-rouge">splice/golden/unicode</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§9.5</td>
      <td>orphaned slots are dropped with their text printed; <code class="language-plaintext highlighter-rouge">--rename-slot</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/slots/orphans</code>, <code class="language-plaintext highlighter-rouge">splice/slots/rename</code>, <code class="language-plaintext highlighter-rouge">splice/golden/slots</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§9.5</td>
      <td>slots declared by position; <code class="language-plaintext highlighter-rouge">migrate-slots</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/slots/found</code>, <code class="language-plaintext highlighter-rouge">splice/slots/outer</code>, <code class="language-plaintext highlighter-rouge">splice/golden/positional-slots</code>, <code class="language-plaintext highlighter-rouge">splice/golden/migrate-slots</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.1</td>
      <td><code class="language-plaintext highlighter-rouge">scan</code> follows <code class="language-plaintext highlighter-rouge">\input</code>, <code class="language-plaintext highlighter-rouge">\include</code>, <code class="language-plaintext highlighter-rouge">\subfile</code>, skips comments, <code class="language-plaintext highlighter-rouge">\verb</code> and <code class="language-plaintext highlighter-rouge">verbatim</code>; malformed markup is an error with a position</td>
      <td><code class="language-plaintext highlighter-rouge">splice/scan/inputs</code>, <code class="language-plaintext highlighter-rouge">splice/scan/comment-skipped</code>, <code class="language-plaintext highlighter-rouge">splice/scan/verb-skipped</code>, <code class="language-plaintext highlighter-rouge">splice/scan/verbatim-skipped</code>, <code class="language-plaintext highlighter-rouge">splice/scan/unclosed-block</code>, <code class="language-plaintext highlighter-rouge">splice/prop/scanner-robustness</code>, <code class="language-plaintext highlighter-rouge">splice/prop/scanner-truncated</code>, <code class="language-plaintext highlighter-rouge">splice/golden/basic</code>, <code class="language-plaintext highlighter-rouge">splice/golden/comments-verbatim</code>, <code class="language-plaintext highlighter-rouge">splice/golden/macro-args</code>, <code class="language-plaintext highlighter-rouge">splice/golden/parse-errors</code>, <code class="language-plaintext highlighter-rouge">splice/golden/outside</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.2</td>
      <td><code class="language-plaintext highlighter-rouge">apply</code> is idempotent, changes nothing outside regions and <code class="language-plaintext highlighter-rouge">sum=</code>, and touches only changed files</td>
      <td><code class="language-plaintext highlighter-rouge">splice/prop/idempotence</code>, <code class="language-plaintext highlighter-rouge">splice/prop/locality</code>, <code class="language-plaintext highlighter-rouge">splice/prop/fixed-point</code>, <code class="language-plaintext highlighter-rouge">splice/golden/basic</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.2</td>
      <td>checksums normalise line endings and trailing whitespace</td>
      <td><code class="language-plaintext highlighter-rouge">splice/prop/normalisation</code>, <code class="language-plaintext highlighter-rouge">splice/normalize/crlf-and-trailing</code>, <code class="language-plaintext highlighter-rouge">splice/golden/crlf</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.2</td>
      <td>hand edits are refused without <code class="language-plaintext highlighter-rouge">--force</code>; nothing is written when there is an error</td>
      <td><code class="language-plaintext highlighter-rouge">splice/prop/edit-detection</code>, <code class="language-plaintext highlighter-rouge">splice/golden/hand-edit</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.2</td>
      <td>missing keys are errors; <code class="language-plaintext highlighter-rouge">--keep-stale</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/failures</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.2</td>
      <td>writes keep line endings and encoding</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/crlf</code>, <code class="language-plaintext highlighter-rouge">splice/golden/unicode</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> reports stale blocks, with <code class="language-plaintext highlighter-rouge">--diff</code></td>
      <td><code class="language-plaintext highlighter-rouge">splice/diff/lines</code>, <code class="language-plaintext highlighter-rouge">splice/golden/slots</code>, <code class="language-plaintext highlighter-rouge">splice/golden/positional-slots</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> reports broken references</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/failures</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> reports untrusted results (splicer side; the extractor fills in the data in M2)</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/failures</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> reports drift; <code class="language-plaintext highlighter-rouge">accept</code> records the new hash</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/drift</code>, <code class="language-plaintext highlighter-rouge">integration/planet-drift</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> warns of undefined macros and orphaned slots</td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§10.3</td>
      <td><code class="language-plaintext highlighter-rouge">check</code> exit codes: non-zero on anything but warnings</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/failures</code>, <code class="language-plaintext highlighter-rouge">splice/golden/config-errors</code>, <code class="language-plaintext highlighter-rouge">splice/golden/slots</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.4</td>
      <td><code class="language-plaintext highlighter-rouge">strip</code> removes markers and keeps generated content</td>
      <td><code class="language-plaintext highlighter-rouge">splice/slots/unwrap</code>, <code class="language-plaintext highlighter-rouge">splice/prop/strip</code>, <code class="language-plaintext highlighter-rouge">splice/golden/strip</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§10.5</td>
      <td>comparator manifests, including <code class="language-plaintext highlighter-rouge">@challenge</code> entries</td>
      <td><code class="language-plaintext highlighter-rouge">splice/golden/manifests</code>, <code class="language-plaintext highlighter-rouge">extract/manifests/challenge-keys</code>, <code class="language-plaintext highlighter-rouge">extract/manifests/challenge-statement-matches</code>, <code class="language-plaintext highlighter-rouge">extract/manifests/unknown-challenge</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Manifests</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§11</td>
      <td>profiles <code class="language-plaintext highlighter-rouge">relative</code> (default), <code class="language-plaintext highlighter-rouge">url</code>, <code class="language-plaintext highlighter-rouge">none</code> for <code class="language-plaintext highlighter-rouge">\leanref</code> and the <code class="language-plaintext highlighter-rouge">meta</code> view</td>
      <td><code class="language-plaintext highlighter-rouge">splice/tex-escape</code>, <code class="language-plaintext highlighter-rouge">splice/config/url-needs-template</code>, <code class="language-plaintext highlighter-rouge">splice/golden/refs</code>, <code class="language-plaintext highlighter-rouge">splice/golden/meta-source</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§11</td>
      <td><code class="language-plaintext highlighter-rouge">check --anonymous</code></td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§12</td>
      <td>every command in the table exists and prints usage</td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§13</td>
      <td>the supported toolchain range is documented and enforced</td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§13</td>
      <td>the same fixture gives the same bundle on every toolchain, apart from <code class="language-plaintext highlighter-rouge">producer</code></td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">extract/golden/ModuleSys</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Trust</code></td>
      <td>M2</td>
    </tr>
    <tr>
      <td>D§13</td>
      <td>the same declaration has the same <code class="language-plaintext highlighter-rouge">stmtHash</code> on every toolchain</td>
      <td><code class="language-plaintext highlighter-rouge">extract/golden/Trust</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Basic</code>, <code class="language-plaintext highlighter-rouge">extract/golden/Manifests</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§13</td>
      <td>the splicer accepts the current and previous bundle schema</td>
      <td><code class="language-plaintext highlighter-rouge">splice/version/schema</code>, <code class="language-plaintext highlighter-rouge">splice/bundle/schema-version</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§14</td>
      <td>testing (this file)</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§15</td>
      <td>repository layout</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§16</td>
      <td>llmbda’s <code class="language-plaintext highlighter-rouge">paper.tex</code> goes through <code class="language-plaintext highlighter-rouge">scan</code> and <code class="language-plaintext highlighter-rouge">strip</code> with every byte outside its blocks kept</td>
      <td><code class="language-plaintext highlighter-rouge">integration/llmbda-scan-strip</code></td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§16</td>
      <td>llmbda parity gate</td>
      <td><code class="language-plaintext highlighter-rouge">imprimatur/parity.sh</code> in llmbda, passed for each of its three documents, then retired with the old exporter (llmbda commit <code class="language-plaintext highlighter-rouge">0114fd4</code>)</td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§16</td>
      <td>PLanet rules figure</td>
      <td><code class="language-plaintext highlighter-rouge">integration/planet-rules</code></td>
      <td>M5</td>
    </tr>
    <tr>
      <td>D§16</td>
      <td>PLanet <code class="language-plaintext highlighter-rouge">check --anonymous</code></td>
      <td>—</td>
      <td>M6</td>
    </tr>
    <tr>
      <td>D§16</td>
      <td>math catalogue comparator manifests import cleanly</td>
      <td><code class="language-plaintext highlighter-rouge">integration/math-manifests</code></td>
      <td>M3</td>
    </tr>
    <tr>
      <td>D§17</td>
      <td>roadmap</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§18.1</td>
      <td>what a document claims</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§18.2</td>
      <td>correctness: the splicer’s laws (Theorem 1)</td>
      <td><code class="language-plaintext highlighter-rouge">splice/prop/locality</code>, <code class="language-plaintext highlighter-rouge">splice/prop/idempotence</code>, <code class="language-plaintext highlighter-rouge">splice/prop/fixed-point</code>, <code class="language-plaintext highlighter-rouge">splice/prop/slot-preservation</code> (property tests; proofs not yet scheduled)</td>
      <td>M1</td>
    </tr>
    <tr>
      <td>D§18.3</td>
      <td>correctness: faithful rendering (Theorem 2)</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§18.4</td>
      <td>checking it: proofs of the splicer’s laws, translation validation of renderings</td>
      <td>— (not yet scheduled)</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§18.5</td>
      <td>the trusted base</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§19</td>
      <td>open questions</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
    <tr>
      <td>D§A</td>
      <td>claims still to check</td>
      <td>—</td>
      <td>n/a</td>
    </tr>
  </tbody>
</table>

<p>The test harness has its own checks (<code class="language-plaintext highlighter-rouge">testkit/harness/counts</code>,
<code class="language-plaintext highlighter-rouge">testkit/gen/splitmix-pinned</code> and so on), which aren’t listed here because
they test the tests.</p>
" }

label gives each block a label made from its key (spaces become -). A key stated again, say in an appendix, gets repeat_suffix on its second label, then the suffix with 2, 3, … on later ones.
template is the content, with {content} for the view’s text, and {label}, {key} and {title} (the block’s second argument). The default is {content}, after a \label line when label is set.
comment = true makes the alias a region delimited by comments, %NAME{key}{title} … %ENDNAME, for places where an environment would disturb TeX, such as a row of a tabbing display. The splicer writes [sum=…] after the marker name.

Options go in the optional argument: view, wrap, label, sum, notation, include, exclude, and the theorem modifiers rule, def, forall and names (views.md). The splicer writes sum= itself.

Where generated content goes

Blocks. If the rest of the header line is blank or a comment, the content starts on the next line. Otherwise it starts right after the header. It ends at the start of the \end{…} line, or at \end itself if something precedes it on that line. Generated content always ends with a newline.
Inline items and references. The content is the second argument.

What the scanner skips

Comments. Markup after % is ignored, but \% is not a comment.
Verbatim text. \verb|…|, \verb*|…|, and the environments verbatim, verbatim*, Verbatim, lstlisting, minted, comment and alltt are skipped. Add other environments with verbatim_envs = […].
Conditionals are not skipped: blocks in a branch that is off are kept up to date like any other. The scanner does note which blocks are typeset, for views that index the paper: not those in a branch that is off (\iffalse, or a switch declared with \newif\ifNAME and set with \NAMEfalse), nor those in a file input only from one.
Definitions. The command named after \newcommand, \providecommand, \NewDocumentCommand, \def and their relatives is being defined, not used, so a paper can define \leancheck itself: \NewDocumentCommand\leancheck{O{} m}{} prints nothing.
Uses without arguments. \leaninline that isn’t followed by [ or { is a definition, as in \newcommand{\x}{\leaninline}, not a use.

Files. The scanner follows \input, \include and \subfile. Paths are relative to the main file’s directory, as in LaTeX, and .tex is added when needed. A file that doesn’t exist is a warning, because it may be generated later.

Checksums and hand edits

Each block and inline item records a checksum of its content in sum=. The checksum is the first 60 bits of the SHA-256, in base64url. It is taken after:

line endings are normalised to \n;
trailing spaces and tabs are removed;
blank lines at both ends are dropped;
slot texts are emptied.

Editing generated content by hand. The checksum then no longer matches. apply refuses to overwrite the block and check reports it, until you either:

move the edit into Lean or into a slot; or
rerun with --force KEY to discard the edit.

Editing a slot is always allowed.

References (\leanref) carry no checksum and are always regenerated.

Slots

A slot’s text is carried over each time the block is regenerated, matched by id and by occurrence. There are two forms:

\leanslot{id}{text}. The id is chosen by the view, usually a constructor name.
Slots by position. Declared in an alias: the given argument of each listed macro is a slot, identified by the text of another argument. This matches existing grammar markup without edits.

A slot that the new content no longer has is dropped, and its text is printed as an orphan-slot warning. --rename-slot OLD=NEW keeps the text when the slot was renamed. migrate-slots --bundle B rewrites slots by position into \leanslot form. It matches each old slot to the new \leanslot inside the macro with the same identifying argument.

Commands

Command	Does
`imprimatur-splice scan [-o requests.json]`	lists every key and view the document asks for, and the document’s inventory: its blocks, with the labels they will get, and its `\label`s, in document order, for views that index the paper
`imprimatur-splice apply --bundle B`	regenerates content. Writes nothing if there is any error. Options: `--force KEY`, `--keep-stale`, `--rename-slot OLD=NEW`, `--profile P`, `--commit SHA`
`imprimatur-splice check --bundle B`	reports what `apply` would change, without writing. Options: `--diff`, `--check-fail-msg MSG`
`imprimatur-splice strip -o DIR`	writes a copy without markers: blocks become their content, wrapped in `wrap` if given; slots become their text; `\leancheck` and `\leanindex` disappear
`imprimatur-splice migrate-slots --bundle B`	see Slots above
`imprimatur build`	`scan`, then `imprimatur-export` in `lean_project`, then `apply`; takes `apply`’s options
`imprimatur check`	the same, with `check` instead of `apply`; writes only the bundle, in `.imprimatur/`
`imprimatur accept KEY…` / `--all`	the same, then records the current statement hashes in `\leancheck` (trust.md)
`imprimatur toolchain install VERSION`	builds the extractor for a toolchain, for external mode

The configuration is imprimatur.toml in the current directory, or --config FILE. With --main FILE.tex, no configuration file is needed.

Exit codes.

Code	Meaning
0	success; warnings allowed
1	`check` or `apply` found an error, or `check` found stale content
2	bad arguments, configuration or bundle

Diagnostics

Every message has a stable code.

Code	Severity	Meaning
`stale`	error (`check`)	content or `sum=` is out of date; `apply` would change it
`hand-edit`	error	generated content was edited by hand
`missing-key`	error, or warning with `--keep-stale`	the bundle has no entry for the key
`missing-view`	error	the entry has no such view, or the view failed to render (the reason is shown)
`bad-ref`	error	a `\leanref` can’t be rendered (no source location, or no `--commit` for a URL)
`bad-content`	error	generated text would break the document: unbalanced braces in an inline item, or `\end{env}` inside a block
`broken-ref`	error	a `\leancheck` key has no entry in the bundle
`untrusted`	error	the result depends on `sorry`, uses an axiom outside `allowed_axioms`, or has untrusted constants in its cone
`drift`	error	a `\leancheck`’s statement changed since it was accepted (trust.md)
`sig-changed`	warning	a `\leancheck`’s statement reads differently but means the same
`no-hash`	error	the bundle has no statement hash for a `\leancheck` key
`not-checked`	warning	`accept` was given a key that no `\leancheck` mentions
`leanok-untrusted`	error	a blueprint node marked `\leanok` depends on an untrusted declaration
`bad-manifest`, `missing-manifest`	error, warning	a comparator manifest can’t be read, or a pattern matches none
`orphan-slot`	warning	a slot disappeared; its text is printed
`missing-input`	warning	an `\input`ed file doesn’t exist
`absolute-input`	warning	an `\input` names an absolute path, which isn’t followed
`outside-project`	warning	`strip` skipped a file reached through `..`, outside the project
`missing-main`	error	the main file doesn’t exist
`parse-error`	error	malformed markup, with its position

This site is open source. Improve this page.