Module emit 

LOGOS source for an imported Lean environment: one literate .lg document — prose headings, literate English forms where they express a declaration exactly, kernel vernacular for the rest — plus the correspondence between Lean and LOGOS names. The document is reparsed and rechecked in a fresh context before anyone may publish it.

What is written

The target’s dependency CLOSURE, every declaration the kernel checked for it: inductives with their constructors, definitions (the importer’s sharing helpers and the recursors LOGOS derived included), theorems with their checked proofs, and axioms. Nothing is written as an assumption that the import checked as a proof, and nothing the import assumed is written as a proof.

How it is checked

1. While the document is built, every declaration is registered in a probe context the moment it is written and compared with the imported declaration, so a failure names the declaration.
2. Before returning, the COMPLETE document is read by Repl::execute_document in a fresh context, the number of commands is counted, every declaration is compared with the imported one — kind, universe parameters, type, and body for a transparent definition, by strict α-equivalence — and the fresh context is searched for anything the document declared that the correspondence does not list.
3. check_statement compares the target’s reparsed type with an independent reference translation of the Lean type (competition rule R8).

Structs

Correspondence

One Lean declaration and the LOGOS declaration that carries it.

EmittedDocument

An emitted document.

Enums

DeclarationKind

What a declaration is, as the kernel holds it.

EmissionFault

Why an emitted document does not reparse to the imported declarations. Every variant names the LOGOS declaration it concerns.

Form

Which surface carries a declaration in the document.

LeanPart

One component of a Lean name.

Origin

Where a LOGOS declaration came from.

Published

What a publication left in place.

Constants

DOCUMENT_EXTENSION

The published document’s extension.

FAILURE_EXTENSION

The extension of a failed run’s diagnostic record.

MAX_SOURCE_BYTES

The largest document the emitter writes.

Functions

check_statement

Rule R8: the target’s REPARSED statement against reference, an independent translation of the Lean declaration (reference::reference_declaration) in the importer’s names. The reference is carried into LOGOS names through the correspondence alone — the emitter’s own terms play no part — and must name the target, bind the same universe parameters in the same order, and state the same type up to α.

emit_context

emit_document over any checked context whose constants carry the importer’s key scheme. proofs hands back the checked proof of an opaque theorem, which a context does not keep.

emit_document

The dependency closure of target, as a LOGOS document.

publish

Publish outcome under dir/<stem>.lg, or its failure under dir/<stem>.failure.txt.

publish_through

publish, writing every file’s bytes through write — the seam a test uses to make a write fail half way.

verify

Reparse document.source in a fresh context and compare every declaration with what it must be. Returns the checked context.