Module intake 

Intake: the strict front door of a Lean → LOGOS result.

The reader (super) is deliberately tolerant — it is also the Lean Kernel Arena benchmark checker, and reads any 3.1.0 export. Intake is the door a result goes through, and it holds an export to an explicit compatibility rule before any declaration is translated:

• the header names the pinned profile (STAGE_A: Lean 4.14.0, lean4export 3.1.0, format 3.1.0) — an unknown format version is UnsupportedExportVersion, any other producer is UnsupportedToolchain;
• every record has exactly the fields format 3.1.0 defines for its kind — an unknown field is UnknownField, a missing or mistyped one MalformedExport, an unknown kind UnknownRecordKind, a metavariable or free variable UnresolvedMetavariable;
• every referenced constant is declared (MissingDeclaration) and none is declared twice (DuplicateDeclaration).

It also answers the question retention, emission and packaging share: which declarations does a target depend on (Intake::closure), in dependency order.

Structs

Declaration

One declared constant.

Header

The export’s first record.

Intake

An export that passed intake.

Profile

The toolchain and assumption profile a result is produced under.

Enums

Component

One component of a Lean name.

DeclarationKind

What a declaration record declares.

Constants

EXPORTER_FLAGS

The exporter flags every result is produced with: metadata and unsafe declarations are exported so that the reader, not the exporter, decides what they mean.

EXPORTER_REVISION

The pinned lean4export revision.

EXPORTER_SOURCES

SHA-256 of the pinned exporter’s sources at EXPORTER_REVISION. The exporter is identified by its content, never by the name of the directory holding it.

STAGE_A

Stage A: Lean 4.14.0, lean4export 3.1.0 (revision EXPORTER_REVISION), export format 3.1.0, Lean core only, and Lean’s three standard axioms.

TOOLCHAIN

The elan toolchain name of the pinned Lean.

Functions

components

The components of a kernel identity, when it is the encoding of a Lean name.

encode

The structural encoding of a Lean name, before the reader’s reserved identities apply.

kernel_name

The kernel identity the reader registers the dotted Lean name lean under.

lean_name

The dotted Lean name a kernel identity encodes, as Lean prints it; a kernel name that encodes no Lean name is returned unchanged.

parse_lean_name

Parse a dotted Lean name as Lean prints it: components separated by ., a component that is not an identifier written «…», a component of digits numeric.

print_lean_name

Print components as Lean prints a name.

read

Read and validate an export under profile.

read_header

The header, held to the profile: the format version first (a newer format may legitimately add fields), then the header’s own fields, then the producing toolchain.