Enum ProcessModuleOutcome 

pub enum ProcessModuleOutcome {
    Ok {
        file: ProcessedFile,
        imports: Vec<String>,
    },
    MissingImports {
        file: ProcessedFile,
        imports: Vec<String>,
        missing: Vec<String>,
    },
    HeaderParseFailed {
        diagnostics: LeanElabFailure,
    },
    Unsupported,
}

Outcome of crate::LeanSession::process_module_with_info_tree.

The Lean shim parses the header first (via Lean.Parser.parseHeader) and only runs IO.processCommands if the header parsed cleanly. Ok / MissingImports therefore both carry a populated ProcessedFile (its diagnostics field captures any elaboration failure of the body); HeaderParseFailed short-circuits with just the parser’s diagnostics.

Variants

Ok

Header parsed; every parsed import is present in the session’s open env; the body was processed. imports lists the user-written modules (Lean’s auto-inserted Init is filtered out by the shim).

Fields

file: ProcessedFile

Body projection. file.diagnostics still records any per-command elaboration errors the body produced.

imports: Vec<String>

User-written imports from the file’s header.

MissingImports

Header parsed but some imports name modules the session’s open env does not have. The body was still processed against the available env — file is populated and the partial projection is useful diagnostic data. Callers typically surface missing as a warning.

Fields

file: ProcessedFile

Body projection (partial if some declarations depended on the missing modules).

imports: Vec<String>

User-written imports from the file’s header.

missing: Vec<String>

Subset of imports not present in the session’s open env.

HeaderParseFailed

Lean.Parser.parseHeader reported error-severity messages. IO.processCommands was not invoked; only the header diagnostics are returned.

Fields

diagnostics: LeanElabFailure

Header-parser diagnostics, with the same byte-budget semantics as crate::host::evidence::LeanKernelOutcome::Rejected.

Unsupported

The capability dylib does not export the lean_rs_host_process_module_with_info_tree shim. No FFI call was made.

Trait Implementations

impl Debug for ProcessModuleOutcome

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'lean> TryFromLean<'lean> for ProcessModuleOutcome

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.