Diagnostics and Observability

lean-rs and lean-rs-host project errors to the same stable [lean_rs::LeanDiagnosticCode] taxonomy and emit structured tracing spans against the lean_rs target. Long-running host session operations can also report live progress through lean_rs_host::LeanProgressSink; see architecture/13-structured-progress.md. lean-rs-worker uses its own LeanWorkerError surface for process-boundary outcomes such as child exit, request timeout, cancellation, data-sink panic, diagnostic-sink panic, and typed command decode failures. A downstream caller gets:

• a stable identifier (err.code()) to react by family, independent of internal stage tags that may grow new variants;
• visibility into where time is spent and where failures originate, without rebuilding the crates.

The taxonomy is unified across lean-rs and lean-rs-host (every recoverable failure on either side maps to a stable code); the span catalogue is split by emitting crate so the layer boundary is visible at the log line. Lean internal panics are outside this error taxonomy: there is no SessionPoisoned code. A Lean runtime panic during a LeanSession call may terminate the process; see architecture/06-panic-containment.md. When the same failure happens inside lean-rs-worker, the parent observes a typed worker exit instead of an in-process LeanDiagnosticCode.

Diagnostic codes

The enum is #[non_exhaustive]; new variants may be added. Variant names and as_str() ids are stable across patch releases.

Loader preflight

Manifest-backed shipped capabilities can be checked before LeanCapability opens any dylib:

#![allow(unused)]
fn main() {
let report = lean_rs::LeanCapabilityPreflight::new(
    lean_rs::LeanBuiltCapability::manifest_path(env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST")),
)
.check();

if let Some(check) = report.first_error() {
    eprintln!("{}: {}", check.code(), check.repair_hint());
}
}

LeanCapability::from_build_manifest runs the same preflight internally when that produces a clearer failure. The broad LeanError still reports LeanDiagnosticCode::ModuleInit, but the bounded message includes the stable loader code and repair hint.

Normal users should not repair shipped apps by setting LD_LIBRARY_PATH or DYLD_*. A missing search path in the canonical flow is a packaging or artifact-manifest problem, not a caller-managed loader-flag problem.

Worker bootstrap checks

Packaged worker applications can check deployment state before running a real command:

#![allow(unused)]
fn main() {
let report = builder.check();
if let Some(check) = report.first_error() {
    eprintln!("{}: {}", check.code(), check.repair_hint());
}
}

LeanWorkerCapabilityBuilder::check() validates the app-owned worker child, manifest-backed capability artifact, protocol handshake, import session, and optional metadata expectation. It returns LeanWorkerBootstrapReport, not raw child pids, pipe handles, protocol frames, loader flags, or std::process configuration.

Internal covers Rust callback panics caught before they unwind across C or Lean. It does not mean a Lean kernel/runtime panic was contained. Those failures require a worker-process boundary.

L1 callback shims also return LeanCallbackStatus for callback-local outcomes. Ok = 0 continues the Lean-side callback loop; StaleHandle = 1 means Lean called a dropped handle; Panic = 2 means Rust contained a callback panic and recorded LeanError::Host on the live handle; WrongPayload = 3 means Lean used a handle with the wrong payload trampoline; and Stopped = 4 means the Rust callback asked Lean to stop cleanly.

lean-toolchain uses a separate LinkDiagnostics enum for build-script work. Those diagnostics cover Lean discovery, unsupported toolchains, missing lake, missing Lake targets, Lake build failures, and unresolved Lake outputs. They render as one line so a build.rs can either return them or print them through cargo:warning=.

Cancelled is cooperative. It is returned only when lean-rs-host regains control and checks the token; it does not pre-empt an in-flight Lean call. See architecture/07-cooperative-cancellation.md.

Progress sink panics are caught at the Rust callback boundary and surfaced as LeanError::Host with stage CallbackPanic, code lean_rs.internal.

Worker process diagnostics and pool snapshots

lean-rs-worker deliberately uses a separate worker error surface for process boundary failures. Child panic/abort, request timeout, cancellation-triggered cycle, stale lease use, row sink panic, diagnostic sink panic, and typed command decode failure are worker outcomes, not LeanDiagnosticCode values from the in-process host stack.

For large local runs, use LeanWorkerPoolSnapshot and LeanWorkerSessionLease::snapshot() for operational state. Snapshots summarize queue depth, active workers, warm leases, restart reasons, best-effort child RSS, stream outcomes, delivered row counts, payload bytes, elapsed stream time, and backpressure counters. They intentionally do not expose child pids, worker ids, pipe handles, protocol frames, or scheduling internals.

Matching on codes

LeanError, LeanElabFailure, and LeanMetaResponse all project to the same taxonomy via .code():

#![allow(unused)]
fn main() {
use lean_rs::{LeanDiagnosticCode, LeanError};

fn report(err: &LeanError) {
    match err.code() {
        LeanDiagnosticCode::Linking => eprintln!("rebuild the capability: {err}"),
        LeanDiagnosticCode::ModuleInit => eprintln!("check `lake build` produced the dylib: {err}"),
        LeanDiagnosticCode::LeanException => {
            if let LeanError::LeanException(exc) = err {
                eprintln!("Lean raised {:?}: {}", exc.kind(), exc.message());
            }
        }
        LeanDiagnosticCode::Cancelled => eprintln!("caller cancelled the operation"),
        other => eprintln!("unhandled {other}: {err}"),
    }
}
}

LeanMetaResponse::code() returns an Option: None on Ok, Some(Unsupported) when the capability lacked the requested service, and Some(Elaboration) on the other two failure shapes (which carry a LeanElabFailure). LeanElabFailure::code() always returns Elaboration.

Tracing

lean-rs and lean-rs-host declare spans against the lean_rs target. Neither installs a subscriber—pick one downstream, or use DiagnosticCapture for tests.

Recommended RUST_LOG scopes:

info covers init, library open, and session import (once-per-cycle events). debug adds per-session-method dispatch (query_declaration, elaborate, kernel_check, bulk methods, pool acquire/release). trace adds per-dispatch (LeanExported::call) and per-decoder events.

A typical tracing-subscriber wire-up:

#![allow(unused)]
fn main() {
tracing_subscriber::fmt()
    .with_env_filter(
        tracing_subscriber::EnvFilter::try_from_default_env()
            .unwrap_or_else(|_| tracing_subscriber::EnvFilter::new("lean_rs=info")),
    )
    .init();
}

Spans emitted by lean-rs (L1)

FFI-primitive spans: init, library open, module initializer, typed-export dispatch, ABI decode. Fire whether the caller is lean-rs-host or any other downstream of lean-rs.

Spans emitted by lean-rs-host (L2)

Host-stack session and pool spans. Fire only if the caller opted into the L2 stack and is driving a session.

Capturing diagnostics in tests

DiagnosticCapture is an in-process buffer for spans and events emitted against the lean_rs target. Thread-local and bounded; the guard restores the previous subscriber on Drop.

#![allow(unused)]
fn main() {
use lean_rs::{DiagnosticCapture, LeanDiagnosticCode, LeanRuntime};
use lean_rs_host::LeanHost;

#[test]
fn rebuild_advice_fires_on_missing_dylib() {
    let capture = DiagnosticCapture::install();

    let runtime = LeanRuntime::init().unwrap();
    let host = LeanHost::from_lake_project(runtime, "/path/to/lake").unwrap();
    let err = host
        .load_capabilities("my_pkg", "DefinitelyMissingLib")
        .expect_err("missing dylib must fail");

    assert_eq!(err.code(), LeanDiagnosticCode::ModuleInit);

    let events = capture.events();
    assert!(events.iter().any(|e| e.span.as_deref()
        == Some("lean_rs.module.library.open")));
}
}

The guard is !Send + !Sync: it pins to the installing thread. Default capacity is 256 events; over-capacity drops the oldest entry and bumps capture.overflowed(). Use DiagnosticCapture::with_capacity(N) for larger budgets. Scope is just lean_rs; events from other crates pass through untouched.

Redaction and bounding

Two values can grow without bound: Lean-authored text (capability messages, diagnostic messages) and filesystem paths. Both are bounded at the construction site:

• Lean-authored strings pass through bound_message (the same 4 KiB cap that protects LeanError::message). Enforced on the UTF-8 char boundary, so multibyte sequences are never split.
• Filesystem paths emitted as span fields are shortened to the basename plus up to two parent components (build/lib/lib.dylib). The full absolute path is only emitted at trace level by call sites that explicitly need it.

Paths are not treated as secrets; shortening is a bounding decision, not a redaction decision. If a downstream policy requires full path suppression, install a tracing-subscriber filter that drops the relevant fields.

Cross-references

• lean_rs::LeanDiagnosticCode—the enum; defined on L1, lean-rs and lean-rs-host project to it.
• lean_rs::DiagnosticCapture—the in-process capture; captures spans from lean-rs and lean-rs-host against the shared lean_rs target.
• Host stack surface—methods on LeanSession and SessionPool that emit the L2 spans above.
• Concurrency contract—why spans are per-thread.
• Safety model—why messages are bounded at construction.
• Panic containment—why Lean internal panics are process-scoped.
• Cooperative cancellation—where cancellation tokens are checked and what they cannot interrupt.
• Callback registry—how L1 callback statuses relate to the error taxonomy.
• Interop build and link—typed lean-toolchain build diagnostics and cache behavior.
• Structured progress—live in-process progress events for long-running host calls.