Enum LeanDiagnosticCode 

#[non_exhaustive]
pub enum LeanDiagnosticCode {
    RuntimeInit,
    Linking,
    ModuleInit,
    SymbolLookup,
    AbiConversion,
    LeanException,
    Elaboration,
    Unsupported,
    Cancelled,
    Internal,
}

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.

#[non_exhaustive] so later prompts may add new families. The variant names and as_str() ids are stable across patch releases.

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

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.

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 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 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

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 LeanDiagnosticCode

impl Eq for LeanDiagnosticCode

impl StructuralPartialEq for LeanDiagnosticCode