Enum HostStage 

#[non_exhaustive]
pub enum HostStage {
    RuntimeInit,
    Conversion,
    CallbackPanic,
    Link,
    Load,
    Internal,
}

What the host stack was doing when it failed.

A flat tag enum; callers rarely match on it and read HostFailure::message instead. Use LeanDiagnosticCode for the stable, caller-facing failure taxonomy — HostStage is the host-stack’s internal classification and may grow new variants when new internal paths are added. Marked #[non_exhaustive] so later prompts can add variants without breaking exhaustive matches.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

RuntimeInit

OnceLock + lean_initialize_* panic-or-failure.

Conversion

First-order ABI value malformed (wrong kind, out of range, invalid UTF-8, non-scalar char).

CallbackPanic

A Rust panic was contained at a Lean → Rust callback boundary.

Link

Link-time failure (missing symbol, header-digest mismatch).

Load

Load-time failure (dlopen, per-module initializer).

Internal

A pub(crate) invariant tripped. Indicates a bug in lean-rs.

Trait Implementations

impl Clone for HostStage

fn clone(&self) -> HostStage

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for HostStage

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

Formats the value using the given formatter.

impl PartialEq for HostStage

fn eq(&self, other: &HostStage) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for HostStage

impl Eq for HostStage

impl StructuralPartialEq for HostStage