Module error 

Typed error boundary for the safe lean-rs surface.

Every fallible public function returns LeanResult<T>. LeanError is the single error type that crosses the boundary; it has three variants:

• LeanError::LeanException when Lean threw through its IO error channel. The payload reports the IO.Error constructor as LeanExceptionKind and a bounded message() that callers may surface to end users.
• LeanError::Host when our stack failed (init, ABI conversion, contained callback panic, future link/load, internal invariant). The payload reports the HostStage and a bounded developer-facing message().
• LeanError::Cancelled when a lean-rs-host cooperative cancellation token was observed before an FFI dispatch or between bulk dispatches.

Bounded messages are a structural invariant: LeanException and HostFailure have private fields, and the only constructors are pub(crate); both run a shared helper that truncates the message at LEAN_ERROR_MESSAGE_LIMIT on a UTF-8 char boundary. LeanCancelled also has private fields and carries a fixed host-authored message. External callers receive LeanError values but cannot mint one with an unbounded message.

The rule callers learn: runtime / host failures are LeanError; application semantics are values. A Lean function returning IO (Except E T) decodes as LeanResult<Result<T, E>> — outer IO failure becomes a LeanError::LeanException, inner Except becomes a Rust Result.

Diagnostic codes

Every error-bearing type on the public surface projects to a stable LeanDiagnosticCode via .code(). The code names the failure family a downstream caller must react to — Linking, Elaboration, Unsupported, and so on — independent of the internal HostStage tag. The as_str() form of each code is the identifier used by the tracing spans and the published docs/diagnostics.md catalogue; variant names and string ids are stable across patch releases.

Structs

CapturedEvent

One captured tracing event.

DiagnosticCapture

Buffered tracing-event collector for the current thread.

HostFailure

A host-stack failure observed inside lean-rs.

LeanCancelled

A cooperative cancellation observed by lean-rs-host.

LeanException

A Lean exception thrown through the IO error channel.

Enums

HostStage

What the host stack was doing when it failed.

LeanDiagnosticCode

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

LeanError

Errors reported across the safe lean-rs boundary.

LeanExceptionKind

Constructor tag for Lean’s IO.Error.

Constants

DIAGNOSTIC_CAPTURE_DEFAULT_CAPACITY

Soft cap on the number of events a DiagnosticCapture retains.

LEAN_ERROR_MESSAGE_LIMIT

Hard cap on the byte length of any LeanError message.

Type Aliases

LeanResult

Result alias used by every fallible public API in lean-rs.