Enum LeanDiagnosticCode 

pub enum LeanDiagnosticCode {
    RuntimeInit,
    Linking,
    ModuleInit,
    SymbolLookup,
    AbiConversion,
    LeanException,
    Elaboration,
    Unsupported,
    Cancelled,
    Internal,
    ResourceExhausted,
}

Stable, caller-facing classification of a lean-rs failure.

Every error-bearing public type projects to one of these via .code():

• LeanError::code—LeanException → LeanDiagnosticCode::LeanException, Host → the code recorded by the construction site.
• lean_rs_host::LeanElabFailure::code—always LeanDiagnosticCode::Elaboration.
• lean_rs_host::meta::LeanMetaResponse::code—Ok → None, Failed / TimeoutOrHeartbeat → Elaboration, Unsupported → Unsupported.

Use match err.code() { Linking => ..., ModuleInit => ..., _ => ... } to react by family; reach for HostStage only when you need the host-stack’s internal classification (and accept that it may grow new variants). The string form returned by Self::as_str is also the identifier emitted in tracing fields and listed in docs/diagnostics.md. Variant names and as_str() ids are stable across patch releases.

Variants

RuntimeInit

Lean runtime initialization failed (panic in lean_initialize, thread-attach floor failure, task-manager init failure).

Linking

A linkable artefact was missing or did not match: a Lake package/module name was invalid, the initializer symbol was absent, or the header digest did not match the active toolchain.

ModuleInit

A capability dylib could not be opened, parsed, or its root module initializer raised. Also: the Lake project root did not exist or was not a directory.

SymbolLookup

A function or global symbol was not present in the loaded dylib when a session call tried to resolve it.

AbiConversion

An ABI conversion failed: wrong Lean kind for the requested Rust type, integer out of range, invalid UTF-8, or a queried declaration was missing from the imported environment.

LeanException

Lean raised through its IO error channel. Inspect LeanException::kind for the IO.Error constructor.

Elaboration

Term parsing or elaboration produced one or more diagnostics. The payload is a lean_rs_host::LeanElabFailure with the typed diagnostic list.

Unsupported

The loaded capability does not expose the requested service— either the Lean shim returned unsupported for the request shape, or the optional capability symbol was absent at load time.

Cancelled

A cooperative cancellation token was observed before dispatch.

Internal

A pub(crate) invariant tripped, or a callback panicked inside the safe boundary. Indicates a bug in lean-rs.

ResourceExhausted

A caller-configured resource budget was exhausted before the operation ran.

Implementations

impl LeanDiagnosticCode

pub const fn as_str(self) -> &'static str

Stable identifier used in tracing fields and docs/diagnostics.md.

The returned string is part of the published API; the value for an existing variant is fixed across patch releases. New variants may add new ids.

pub const fn description(self) -> &'static str

One-line prose description used in docs/diagnostics.md and as the default fallback when a span needs human-readable context.

Trait Implementations

impl Clone for LeanDiagnosticCode

fn clone(&self) -> LeanDiagnosticCode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for LeanDiagnosticCode

impl Debug for LeanDiagnosticCode

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

Formats the value using the given formatter.

impl Display for LeanDiagnosticCode

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

Formats the value using the given formatter.

impl Eq for LeanDiagnosticCode

impl Hash for LeanDiagnosticCode

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for LeanDiagnosticCode

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LeanDiagnosticCode