Module pipeline 

The Lean → LOGOS pipeline, one named stage at a time, and the benchmark protocol’s dispatch.

Parsing and validation (intake), environment import and checking (the reader), audit construction (ImportReport), assumption policy, emission (emit) and packaging (package) stay separate here, each recording its own receipt stage, so a result is never one unexplained Boolean (competition rule R1). The reader interleaves translation and checking per declaration; that is reported honestly — a declaration the kernel refused leaves translated not_run, since the closure’s translation never finished.

Everything here is pure: no file, process or clock. Reading the export, running Lean, publishing the package and replaying it in a fresh process are the command’s (largo lean).

Structs

Checked

A result and, when every stage up to packaging passed, the package to publish and replay.

Diagnostic

One typed, located diagnostic of a result.

LeanResult

A logos-lean-result/1 document under construction.

Limits

Budgets declared before any work.

Loss

Information the result does not carry from the Lean input.

PackageRef

A published package, as the result names it.

Enums

LeanEvidence

What the run observed of Lean itself.

Constants

RESULT_SCHEMA

Functions

check_export

Run every in-process stage over a Lean export for the dotted Lean name target: intake, import and check, independent recheck, assumption policy, emission and package assembly. fresh_replay is left to the caller, which must replay the published package in a new process.

run_cli

The Lean Kernel Arena benchmark protocol: one input path, ACCEPT on stdout and exit 0 on acceptance, exit 1 on rejection, exit 2 on decline. Kept byte-for-byte for benchmark consumers.

self_verification_failure

A refusal of LOGOS’s own artifact — emission, packaging, replay — once every check of the user’s input passed. Unsupported capabilities, budgets and environment failures keep their codes; any other refusal (a rejection, a malformed or ill-typed artifact of our own making) is an InternalInconsistency: the fault is ours, and it is never reported as the user’s mathematics being wrong.