The emitter

Produces emission/1.0 — a machine-readable inventory of everything a topic library declares, with each declaration's full transitive axiom closure.

It never parses Lean source, and that is the whole point

Every fact here is read out of Environment.constants and Lean.collectAxioms in the environment that actually elaborated. No regex, no line scanning, no declaration-site heuristics.

That is not a style preference. A source-parsing extractor is defeated by declaration syntax: the legal forms

set_option maxHeartbeats 400000 in theorem sneaky : False := by sorry
open Classical in theorem sneaky : False := by sorry

are matched by neither the declaration-site nor the declaration-name regex in the corpus server's Lean auditor — reproduced by executing them, which returned a clean verdict for a sorry-backed proof. An environment sweep cannot fail that way, because it never sees syntax. sneaky is a constant like any other, and its axiom closure contains sorryAx.

Scoping is by module, never by name prefix

A declaration at the root namespace, or under a foreign namespace, sitting inside a topic module still lands in the .olean and is importable downstream. A name-prefix scope misses it, and a mis-set prefix yields an empty decls[] — a vacuous pass observationally identical to a clean build. Both failure modes are closed by scoping to the module set and refusing to emit an empty scope.

Determinism

Neither Environment.constants iteration order nor collectAxioms output order is specified. Measured on this toolchain, collectAxioms returned [propext, Quot.sound, Classical.choice] for one declaration and [Quot.sound, propext, Classical.choice] for the next in the same run. Every array this file writes is therefore sorted before serialization, and the constant list is sorted by name. Two runs over an unchanged environment produce byte-identical output except for emitted_at.

No digests

Lean core at v4.32.1 ships no SHA-256, and Lake's Hash is a 64-bit non-cryptographic value that is not portable across toolchains. All contract digests are computed downstream by mfc, from these bytes, so canonicalization lives in exactly one language.

Wire encodings

def MathFormalContract.ppOpts : Lean.Options

Pretty-printer options, pinned for digest stability.

format.width must be pinned. Measured type_pp on this toolchain contains hard line breaks at the wrap width:

"∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]\n  [inst_1 : ...]"

so an unpinned width silently rotates every downstream statement digest on a toolchain that changes its default. mfc additionally whitespace-normalizes before hashing; this is belt and braces.

pp.proofs must be true, and its default is false. With the default, every proof subterm prints as ⋯ — and value_pp is emitted for def and opaque, where statement_digest hashes it. So the default was deleting content from a digest input: two defs differing only inside an elided proof would hash identically. Measured on this package's own emission, 13 of 150 constants came out elided, every one of them a compiler-generated def (.noConfusion, .elim, ._sparseCasesOn_N) whose body carries proofs.

mfc lint rule E-07 is what found it, which is the arrangement working: the rule states the property, the emitter has to satisfy it. pp.proofs accounts for proof elisions. pp.deepTerms and an explicit high pp.maxSteps close the two other documented omission paths. The latter matters once the emitter is large enough to emit its own implementation: Lean's default is only 5,000 visited expressions, after which it inserts ⋯ into a definition body.

Ambient options are discarded rather than extended, so a set_option in the caller cannot reach the emitted text.

That discarding is why maxRecDepth has to be set here and not only on the emitter's Core.Context. Core.withOptions recomputes the field from the options it is handed — maxRecDepth := maxRecDepth.get options — so entering this block with a fresh Options silently restores the option default for exactly the ppExpr call that needs the raised one. Measured, not assumed: maxRecDepth.get ({} : Options) is 512, where the Core.Context field it replaces defaults to 1000 — so entering the block did not merely fail to raise the depth, it lowered it. Setting the context field alone therefore looked right and did nothing: derived-alg-geo-lean still failed with maximum recursion depth has been reached on a build whose log shows it checked out the commit that set it. Zero is Lean's documented no-limit sentinel for this option, and withIncRecDepth special-cases it (max != 0 && curr == max).

Equations

• One or more equations did not get rendered due to their size.

Timestamps

def MathFormalContract.isoUtcNow : IO String

emitted_at as ISO-8601 UTC.

Hand-formatted from the field accessors rather than through a format string: the emitter must not acquire a formatting dependency, and a wrong format specifier fails at runtime in Std.Time where a wrong field access fails at compile time.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.sourceGitCommitNow : IO (Option String)

The commit of the source checkout this sweep describes, or none when the working directory is not a git repository.

Never an error: provenance binding is mfc bundle's gate (it refuses an environment whose root_package.rev disagrees with this stamp), and an honest artifact must still be produced outside a checkout -- the field is simply omitted and bundle has nothing to compare. The 40-hex check keeps a misconfigured git from stamping an error message as a commit.

Equations

• One or more equations did not get rendered due to their size.

The sweep

Phase timing

Nanosecond subtotals for the sweep. They go to stderr and nowhere else. Putting them in emission/1.0 would rotate emission_sha256, break the two-sweep determinism gate the moment a clock ticks differently between runs, and place a measurement of the MACHINE inside a record about the REPOSITORY. Timings are operations telemetry, not evidence, and the two do not share a file.

Forcing is the entire difficulty, and a timer that does not force reads zero. Lean evaluates PrettyPrinter.ppExpr's result lazily. A draft of this instrumentation reported the whole sweep at single-digit milliseconds and attributed the cost to Json.pretty in the driver -- which is where the thunks were being demanded, not where the work belonged. Every counter below is therefore paired with a SIZE, and computing that size is what demands the thunk: String.length walks the UTF-8 bytes (utf8ByteSize would not, being O(1) off the header), and Array.size demands the array qsort had to build. Reporting the sizes is also what stops the compiler eliminating the force.

The forcing cost sits inside the number it forces, deliberately. pp_ms includes the walk over the text ppExpr produced, because excluding it would report a delaboration cost for text nothing had yet materialized.

def MathFormalContract.inScopeModulesForRoots (env : Lean.Environment) (roots : List Lean.Name) : Std.HashSet Lean.Name

The module set in scope for one or more library roots: each root module and everything below it. A topic monorepo can therefore keep a thin combined umbrella while sweeping the declarations owned by each constituent library.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.inScopeModules (env : Lean.Environment) (rootLib : Lean.Name) : Std.HashSet Lean.Name

The module set in scope for rootLib: the root module itself and everything under it.

Equations

• MathFormalContract.inScopeModules env rootLib = MathFormalContract.inScopeModulesForRoots env [rootLib]

def MathFormalContract.emitJsonForRoots (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (externals : Array Lean.Name) (leanOptions : List (String × Lean.Json)) (emittedAt : String) (sourceGitCommit : Option String := none) : Lean.MetaM (Lean.Json × Nat)

Build the emission/1.0 document over the ambient environment.

Returns the document and the number of constants whose axiom closure contains sorryAx. The caller decides what to do about that count; this function does not throw on it, because the artifact must be written even when — especially when — the answer is "this repo currently has three sorries".

Throws only on an empty module scope, which is not a state to report but a misconfiguration: it is the observable signature of a mis-set rootLib, and it must not be able to produce a passing artifact.

leanOptions is declared by the caller, not observed, and that is a limitation worth stating rather than hiding. Elaboration options are compile flags; they are not recorded in the .olean, so an emitter that imports a module cannot recover the options that built it. Reading the ambient options instead — which an earlier draft did — makes the artifact report the emitter process's defaults: measured, this package emitted autoImplicit: true while its own lakefile.toml sets it false. A trust record whose first job is to stop false claims must not open with one. So the caller declares them, in the same generated file that a topic's lakefile.toml is rendered beside, and mfc lint cross-checks the two.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.emitJson (rootLib : Lean.Name) (leanOptions : List (String × Lean.Json)) (emittedAt : String) (sourceGitCommit : Option String := none) : Lean.MetaM (Lean.Json × Nat)

Build emission/1.0 for a conventional single-root library.

Equations

• MathFormalContract.emitJson rootLib leanOptions emittedAt sourceGitCommit = MathFormalContract.emitJsonForRoots rootLib [] #[] leanOptions emittedAt sourceGitCommit

Driver

@[implemented_by _private.MathFormalContract.Emit.0.MathFormalContract.emitToFileForRootsImpl]

opaque MathFormalContract.emitToFileForRoots (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (externals : Array Lean.Name) (leanOptions : List (String × Lean.Json)) (outPath : System.FilePath) : IO UInt32

Import rootLib, sweep it, and write emission/1.0 to outPath.

unsafe is confined to the implementation rather than propagated to callers. enableInitializersExecution is an unsafe primitive, and without it the sweep reads empty environment extensions; forcing every consumer to write unsafe def main would push that detail into the three lines a topic repo generates, which are meant to be the one piece of Lean nobody has to think about.

def MathFormalContract.emitToFile (rootLib : Lean.Name) (leanOptions : List (String × Lean.Json)) (outPath : System.FilePath) : IO UInt32

Import and sweep a conventional single-root library.

Equations

• MathFormalContract.emitToFile rootLib leanOptions outPath = MathFormalContract.emitToFileForRoots rootLib [] #[] leanOptions outPath

def MathFormalContract.emitMainForRoots (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (leanOptions : List (String × Lean.Json)) (args : List String) : IO UInt32

The entry point for a monorepo whose combined root is a declaration-free umbrella. additionalRoots names the constituent module trees to include.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.emitMain (rootLib : Lean.Name) (leanOptions : List (String × Lean.Json)) (args : List String) : IO UInt32

The entry point a topic repo calls, with its root library and its elaboration options hard-coded.

Both are parameters of the generated file, not flags, on purpose. A --root a caller can retype is a scope a caller can silently shrink, and a shrunk scope is the vacuous pass this whole artifact exists to make impossible. A --lean-option a caller can retype is a claim about the build that the build did not make. Both are rendered from the same copier answers as the topic's lakefile.toml, so the two files agree by construction and mfc lint fails them if they ever stop agreeing.

Equations

• MathFormalContract.emitMain rootLib leanOptions args = MathFormalContract.emitMainForRoots rootLib [] leanOptions args