Skip to main content

lean_rs/error/
mod.rs

1//! Typed error boundary for the safe `lean-rs` surface.
2//!
3//! Every fallible public function returns [`LeanResult<T>`]. [`LeanError`]
4//! is the single error type that crosses the boundary; it has three
5//! variants:
6//!
7//! - [`LeanError::LeanException`] when Lean threw through its `IO` error
8//!   channel. The payload reports the `IO.Error` constructor as
9//!   [`LeanExceptionKind`] and a bounded `message()` that callers may
10//!   surface to end users.
11//! - [`LeanError::Host`] when our stack failed (init, ABI conversion,
12//!   contained callback panic, future link/load, internal invariant). The
13//!   payload reports the [`HostStage`] and a bounded developer-facing
14//!   `message()`.
15//! - [`LeanError::Cancelled`] when a `lean-rs-host` cooperative
16//!   cancellation token was observed before an FFI dispatch or between
17//!   bulk dispatches.
18//!
19//! Bounded messages are a *structural* invariant: [`LeanException`] and
20//! [`HostFailure`] have private fields, and the only constructors are
21//! `pub(crate)`; both run a shared helper that truncates the message at
22//! [`LEAN_ERROR_MESSAGE_LIMIT`] on a UTF-8 char boundary. [`LeanCancelled`]
23//! also has private fields and carries a fixed host-authored message.
24//! External callers receive `LeanError` values but cannot mint one with
25//! an unbounded message.
26//!
27//! The rule callers learn: **runtime / host failures are [`LeanError`];
28//! application semantics are values.** A Lean function returning
29//! `IO (Except E T)` decodes as `LeanResult<Result<T, E>>`—outer `IO`
30//! failure becomes a [`LeanError::LeanException`], inner `Except`
31//! becomes a Rust [`Result`].
32//!
33//! ## Diagnostic codes
34//!
35//! Every error-bearing type on the public surface projects to a stable
36//! [`LeanDiagnosticCode`] via `.code()`. The code names the failure
37//! family a downstream caller must react to—`Linking`, `Elaboration`,
38//! `Unsupported`, and so on—independent of the internal [`HostStage`]
39//! tag. The `as_str()` form of each code is the identifier used by the
40//! tracing spans and the published `docs/diagnostics.md` catalogue;
41//! variant names and string ids are stable across patch releases.
42
43use std::any::Any;
44use std::fmt;
45
46pub(crate) mod capture;
47pub(crate) mod io;
48pub(crate) mod panic;
49pub(crate) mod redact;
50
51#[cfg(test)]
52mod tests;
53
54pub use self::capture::{CapturedEvent, DIAGNOSTIC_CAPTURE_DEFAULT_CAPACITY, DiagnosticCapture};
55
56/// Hard cap on the byte length of any [`LeanError`] message.
57///
58/// Enforced at construction time by the `pub(crate)` constructors in this
59/// module. The truncation respects UTF-8 char boundaries, so the cap is
60/// an upper bound rather than an exact length.
61pub const LEAN_ERROR_MESSAGE_LIMIT: usize = 4096;
62
63/// Result alias used by every fallible public API in `lean-rs`.
64pub type LeanResult<T> = Result<T, LeanError>;
65
66/// Errors reported across the safe `lean-rs` boundary.
67#[derive(Clone, Debug)]
68pub enum LeanError {
69    /// Lean threw through its `IO` error channel; see [`LeanException`].
70    LeanException(LeanException),
71    /// The host stack failed at a particular stage; see [`HostFailure`].
72    Host(HostFailure),
73    /// A cooperative cancellation token was observed before dispatch.
74    Cancelled(LeanCancelled),
75}
76
77impl LeanError {
78    /// Project to the stable [`LeanDiagnosticCode`] taxonomy.
79    ///
80    /// `LeanException` always maps to [`LeanDiagnosticCode::LeanException`];
81    /// `Host` returns the code recorded by the construction site.
82    #[must_use]
83    pub fn code(&self) -> LeanDiagnosticCode {
84        match self {
85            Self::LeanException(_) => LeanDiagnosticCode::LeanException,
86            Self::Host(failure) => failure.code,
87            Self::Cancelled(_) => LeanDiagnosticCode::Cancelled,
88        }
89    }
90
91    /// Build a `RuntimeInit` host failure.
92    pub(crate) fn runtime_init(message: impl Into<String>) -> Self {
93        Self::host(HostStage::RuntimeInit, LeanDiagnosticCode::RuntimeInit, message)
94    }
95
96    /// Build a `RuntimeInit` host failure from a caught panic payload.
97    pub(crate) fn runtime_init_panic(payload: &(dyn Any + Send)) -> Self {
98        Self::runtime_init(render_panic_payload(payload))
99    }
100
101    /// Build a `RuntimeInit` host failure for an active Lean toolchain that
102    /// is not in [`lean_rs_sys::SUPPORTED_TOOLCHAINS`]. The build script
103    /// already filters at compile time; this constructor exists for the
104    /// runtime backstop in [`crate::runtime::LeanRuntime::init`].
105    pub(crate) fn runtime_init_unsupported_toolchain(active_version: &str) -> Self {
106        use std::fmt::Write as _;
107        let mut window = String::new();
108        for (i, t) in lean_rs_sys::SUPPORTED_TOOLCHAINS.iter().enumerate() {
109            if i > 0 {
110                window.push_str(", ");
111            }
112            let _ = write!(window, "{:?}", t.versions);
113        }
114        Self::runtime_init(format!(
115            "active Lean toolchain {active_version} is not in the supported window: {window}",
116        ))
117    }
118
119    /// Build a `Linking` host failure (missing/invalid Lake names,
120    /// missing initializer symbol, header-digest mismatch).
121    pub(crate) fn linking(message: impl Into<String>) -> Self {
122        Self::host(HostStage::Link, LeanDiagnosticCode::Linking, message)
123    }
124
125    /// Build a `ModuleInit` host failure (dylib could not be opened,
126    /// initializer raised, Lake project path bad).
127    pub(crate) fn module_init(message: impl Into<String>) -> Self {
128        Self::host(HostStage::Load, LeanDiagnosticCode::ModuleInit, message)
129    }
130
131    /// Build a `ModuleInit` host failure from a caught panic payload.
132    pub(crate) fn module_init_panic(payload: &(dyn Any + Send)) -> Self {
133        Self::module_init(render_panic_payload(payload))
134    }
135
136    /// Build a `SymbolLookup` host failure (dlsym miss, signature
137    /// mismatch—function symbol expected but global found, etc.).
138    pub(crate) fn symbol_lookup(message: impl Into<String>) -> Self {
139        Self::host(HostStage::Link, LeanDiagnosticCode::SymbolLookup, message)
140    }
141
142    /// Build an `AbiConversion` host failure (wrong Lean kind, integer
143    /// out of range, invalid UTF-8, missing declaration).
144    pub(crate) fn abi_conversion(message: impl Into<String>) -> Self {
145        Self::host(HostStage::Conversion, LeanDiagnosticCode::AbiConversion, message)
146    }
147
148    /// Build a Lean-thrown-exception report with a bounded message.
149    pub(crate) fn lean_exception(kind: LeanExceptionKind, message: impl Into<String>) -> Self {
150        Self::LeanException(LeanException {
151            kind,
152            message: bound_message(message.into()),
153        })
154    }
155
156    /// Build a host-stack failure from a caught `std::panic::catch_unwind`
157    /// payload at a Lean → Rust callback boundary. The payload is
158    /// rendered into a string before bounding so the panic value never
159    /// escapes the error boundary.
160    pub(crate) fn callback_panic(payload: &(dyn Any + Send)) -> Self {
161        Self::host(
162            HostStage::CallbackPanic,
163            LeanDiagnosticCode::Internal,
164            render_panic_payload(payload),
165        )
166    }
167
168    /// Build an internal host failure for a `pub(crate)` invariant breach.
169    pub(crate) fn internal(message: impl Into<String>) -> Self {
170        Self::host(HostStage::Internal, LeanDiagnosticCode::Internal, message)
171    }
172
173    /// Build a resource-exhaustion host failure for caller-configured limits.
174    pub(crate) fn resource_exhausted(message: impl Into<String>) -> Self {
175        Self::resource_exhausted_with_facts(message, None)
176    }
177
178    /// Build a resource-exhaustion host failure with structured runtime facts.
179    pub(crate) fn resource_exhausted_with_facts(
180        message: impl Into<String>,
181        facts: Option<ResourceExhaustedFacts>,
182    ) -> Self {
183        Self::Host(HostFailure {
184            stage: HostStage::Resource,
185            code: LeanDiagnosticCode::ResourceExhausted,
186            message: bound_message(message.into()),
187            resource_facts: facts.map(Box::new),
188        })
189    }
190
191    /// Build a cooperative cancellation report.
192    pub(crate) fn cancelled() -> Self {
193        Self::Cancelled(LeanCancelled {
194            message: "operation cancelled by LeanCancellationToken".to_owned(),
195        })
196    }
197
198    /// Shared host-failure constructor. Private—every call site uses
199    /// the typed wrappers above so the [`HostStage`] / [`LeanDiagnosticCode`]
200    /// pair cannot drift.
201    fn host(stage: HostStage, code: LeanDiagnosticCode, message: impl Into<String>) -> Self {
202        Self::Host(HostFailure {
203            stage,
204            code,
205            message: bound_message(message.into()),
206            resource_facts: None,
207        })
208    }
209}
210
211impl fmt::Display for LeanError {
212    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
213        match self {
214            Self::LeanException(e) => write!(f, "lean-rs: {e}"),
215            Self::Host(e) => write!(f, "lean-rs: {e}"),
216            Self::Cancelled(e) => write!(f, "lean-rs: {e}"),
217        }
218    }
219}
220
221impl std::error::Error for LeanError {}
222
223/// A cooperative cancellation observed by `lean-rs-host`.
224///
225/// Constructed only by the crate through the hidden host boundary helper.
226/// The payload is intentionally small and stable: cancellation is a caller
227/// decision, not a Lean diagnostic.
228#[derive(Clone, Debug)]
229pub struct LeanCancelled {
230    message: String,
231}
232
233impl LeanCancelled {
234    /// Caller-facing cancellation message.
235    #[must_use]
236    pub fn message(&self) -> &str {
237        &self.message
238    }
239}
240
241impl fmt::Display for LeanCancelled {
242    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
243        f.write_str(&self.message)
244    }
245}
246
247/// A Lean exception thrown through the `IO` error channel.
248///
249/// Constructed only by the crate; the `kind` and `message` fields are
250/// private so the bounded-message invariant survives downstream
251/// pattern-matching.
252#[derive(Clone, Debug)]
253pub struct LeanException {
254    kind: LeanExceptionKind,
255    message: String,
256}
257
258impl LeanException {
259    /// The `IO.Error` constructor Lean reported.
260    ///
261    /// Use this to classify a Lean-thrown exception when the
262    /// caller-facing taxonomy in [`LeanDiagnosticCode`] is not specific
263    /// enough—for example, distinguishing `FileNotFound` from
264    /// `PermissionDenied` to drive different recovery paths.
265    #[must_use]
266    pub fn kind(&self) -> LeanExceptionKind {
267        self.kind
268    }
269
270    /// What Lean said about the failure, truncated to at most
271    /// [`LEAN_ERROR_MESSAGE_LIMIT`] bytes on a UTF-8 char boundary.
272    #[must_use]
273    pub fn message(&self) -> &str {
274        &self.message
275    }
276}
277
278impl fmt::Display for LeanException {
279    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
280        write!(f, "Lean threw {:?}: {}", self.kind, self.message)
281    }
282}
283
284/// A host-stack failure observed inside `lean-rs`.
285///
286/// Constructed only by the crate; fields are private so the bounded-message
287/// invariant survives downstream pattern-matching.
288#[derive(Clone, Debug)]
289pub struct HostFailure {
290    stage: HostStage,
291    code: LeanDiagnosticCode,
292    message: String,
293    resource_facts: Option<Box<ResourceExhaustedFacts>>,
294}
295
296impl HostFailure {
297    /// The host-stack stage that observed the failure.
298    ///
299    /// This is the *internal* classification; reach for
300    /// [`Self::code`] when displaying a stable identifier or routing on
301    /// the caller-facing failure family. The [`HostStage`] tag may grow
302    /// new variants alongside new internal paths.
303    #[must_use]
304    pub fn stage(&self) -> HostStage {
305        self.stage
306    }
307
308    /// The stable diagnostic code matching this failure.
309    ///
310    /// Recorded at the construction site rather than projected from
311    /// [`Self::stage`], so the code identity does not drift if the
312    /// internal stage tag is later refined. Use this for stable
313    /// logging, metrics, or downstream error routing.
314    #[must_use]
315    pub fn code(&self) -> LeanDiagnosticCode {
316        self.code
317    }
318
319    /// Developer-facing diagnostic, truncated to at most
320    /// [`LEAN_ERROR_MESSAGE_LIMIT`] bytes on a UTF-8 char boundary.
321    #[must_use]
322    pub fn message(&self) -> &str {
323        &self.message
324    }
325
326    /// Structured runtime facts for a resource-boundary refusal, when the
327    /// construction site had them available.
328    #[must_use]
329    pub fn resource_exhausted_facts(&self) -> Option<&ResourceExhaustedFacts> {
330        self.resource_facts.as_deref()
331    }
332}
333
334/// Runtime facts attached to a caller-configured resource refusal.
335///
336/// This type deliberately stays generic enough for the base `lean-rs` crate:
337/// higher layers can attach concrete import-stat diagnostics in the
338/// `last_import_stats` string without forcing a dependency cycle back from
339/// the error core into host or worker crates.
340#[derive(Clone, Debug, Eq, PartialEq)]
341pub struct ResourceExhaustedFacts {
342    pub cause: String,
343    pub work_entered_lean: bool,
344    pub current_rss_kib: Option<u64>,
345    pub limit_kib: Option<u64>,
346    pub import_count: Option<u64>,
347    pub import_limit: Option<u64>,
348    pub requested_imports: Option<u64>,
349    pub last_import_stats: Option<String>,
350}
351
352impl fmt::Display for HostFailure {
353    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
354        write!(
355            f,
356            "host stage {:?} [{}]: {}",
357            self.stage,
358            self.code.as_str(),
359            self.message
360        )
361    }
362}
363
364/// What the host stack was doing when it failed.
365///
366/// A flat tag enum; callers rarely match on it and read
367/// [`HostFailure::message`] instead. Use [`LeanDiagnosticCode`] for the
368/// stable, caller-facing failure taxonomy—`HostStage` is the
369/// host-stack's internal classification and may grow new variants when
370/// new internal paths are added.
371#[derive(Copy, Clone, Debug, Eq, PartialEq)]
372pub enum HostStage {
373    /// `OnceLock` + `lean_initialize_*` panic-or-failure.
374    RuntimeInit,
375    /// First-order ABI value malformed (wrong kind, out of range,
376    /// invalid UTF-8, non-scalar `char`).
377    Conversion,
378    /// A Rust panic was contained at a Lean → Rust callback boundary.
379    CallbackPanic,
380    /// Link-time failure (missing symbol, header-digest mismatch).
381    Link,
382    /// Load-time failure (`dlopen`, per-module initializer).
383    Load,
384    /// A `pub(crate)` invariant tripped. Indicates a bug in `lean-rs`.
385    Internal,
386    /// A caller-configured memory, import, byte, or request budget was exhausted.
387    Resource,
388}
389
390/// Stable, caller-facing classification of a `lean-rs` failure.
391///
392/// Every error-bearing public type projects to one of these via
393/// `.code()`:
394///
395/// - [`LeanError::code`]—`LeanException` → [`LeanDiagnosticCode::LeanException`],
396///   `Host` → the code recorded by the construction site.
397/// - `lean_rs_host::LeanElabFailure::code`—always [`LeanDiagnosticCode::Elaboration`].
398/// - `lean_rs_host::meta::LeanMetaResponse::code`—`Ok` → `None`,
399///   `Failed` / `TimeoutOrHeartbeat` → `Elaboration`, `Unsupported` →
400///   `Unsupported`.
401///
402/// Use `match err.code() { Linking => ..., ModuleInit => ..., _ => ... }`
403/// to react by family; reach for [`HostStage`] only when you need the
404/// host-stack's internal classification (and accept that it may grow new
405/// variants). The string form returned by [`Self::as_str`] is also the
406/// identifier emitted in tracing fields and listed in
407/// `docs/diagnostics.md`. Variant names and `as_str()` ids are stable
408/// across patch releases.
409#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
410pub enum LeanDiagnosticCode {
411    /// Lean runtime initialization failed (panic in `lean_initialize`,
412    /// thread-attach floor failure, task-manager init failure).
413    RuntimeInit,
414    /// A linkable artefact was missing or did not match: a Lake
415    /// package/module name was invalid, the initializer symbol was
416    /// absent, or the header digest did not match the active toolchain.
417    Linking,
418    /// A capability dylib could not be opened, parsed, or its root
419    /// module initializer raised. Also: the Lake project root did not
420    /// exist or was not a directory.
421    ModuleInit,
422    /// A function or global symbol was not present in the loaded dylib
423    /// when a session call tried to resolve it.
424    SymbolLookup,
425    /// An ABI conversion failed: wrong Lean kind for the requested
426    /// Rust type, integer out of range, invalid UTF-8, or a queried
427    /// declaration was missing from the imported environment.
428    AbiConversion,
429    /// Lean raised through its `IO` error channel. Inspect
430    /// [`LeanException::kind`] for the `IO.Error` constructor.
431    LeanException,
432    /// Term parsing or elaboration produced one or more diagnostics.
433    /// The payload is a `lean_rs_host::LeanElabFailure` with the typed
434    /// diagnostic list.
435    Elaboration,
436    /// The loaded capability does not expose the requested service—
437    /// either the Lean shim returned `unsupported` for the request
438    /// shape, or the optional capability symbol was absent at load
439    /// time.
440    Unsupported,
441    /// A cooperative cancellation token was observed before dispatch.
442    Cancelled,
443    /// A `pub(crate)` invariant tripped, or a callback panicked inside
444    /// the safe boundary. Indicates a bug in `lean-rs`.
445    Internal,
446    /// A caller-configured resource budget was exhausted before the operation ran.
447    ResourceExhausted,
448}
449
450impl LeanDiagnosticCode {
451    /// Stable identifier used in tracing fields and `docs/diagnostics.md`.
452    ///
453    /// The returned string is part of the published API; the value for
454    /// an existing variant is fixed across patch releases. New variants
455    /// may add new ids.
456    #[must_use]
457    pub const fn as_str(self) -> &'static str {
458        match self {
459            Self::RuntimeInit => "lean_rs.runtime_init",
460            Self::Linking => "lean_rs.linking",
461            Self::ModuleInit => "lean_rs.module_init",
462            Self::SymbolLookup => "lean_rs.symbol_lookup",
463            Self::AbiConversion => "lean_rs.abi_conversion",
464            Self::LeanException => "lean_rs.lean_exception",
465            Self::Elaboration => "lean_rs.elaboration",
466            Self::Unsupported => "lean_rs.unsupported",
467            Self::Cancelled => "lean_rs.cancelled",
468            Self::Internal => "lean_rs.internal",
469            Self::ResourceExhausted => "lean_rs.resource_exhausted",
470        }
471    }
472
473    /// One-line prose description used in `docs/diagnostics.md` and as
474    /// the default fallback when a span needs human-readable context.
475    #[must_use]
476    pub const fn description(self) -> &'static str {
477        match self {
478            Self::RuntimeInit => "Lean runtime initialization failed",
479            Self::Linking => "a linkable artefact was missing or mismatched",
480            Self::ModuleInit => "a capability dylib could not be opened or initialized",
481            Self::SymbolLookup => "a symbol was not present in the loaded dylib",
482            Self::AbiConversion => "an ABI conversion failed",
483            Self::LeanException => "Lean raised through its IO error channel",
484            Self::Elaboration => "term parsing or elaboration produced diagnostics",
485            Self::Unsupported => "the loaded capability does not expose the requested service",
486            Self::Cancelled => "a cooperative cancellation token was observed before dispatch",
487            Self::Internal => "a pub(crate) invariant tripped — likely a bug in lean-rs",
488            Self::ResourceExhausted => "a caller-configured resource budget was exhausted before dispatch",
489        }
490    }
491}
492
493impl fmt::Display for LeanDiagnosticCode {
494    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
495        f.write_str(self.as_str())
496    }
497}
498
499/// Constructor tag for Lean's `IO.Error`.
500///
501/// 1:1 with `IO.Error` at the active Lean toolchain version (4.29.1—
502/// see `src/lean/Init/System/IOError.lean`), plus an [`Other`] catch-all
503/// for tag values not in the declaration. The crate-internal decoder
504/// maps the raw `lean_obj_tag` to a variant via a `const` table; a unit
505/// test anchors the `userError` mapping against the live Lean runtime
506/// and will fail if the constructor index drifts.
507///
508/// [`Other`]: Self::Other
509#[derive(Copy, Clone, Debug, Eq, PartialEq)]
510pub enum LeanExceptionKind {
511    /// `IO.Error.alreadyExists`
512    AlreadyExists,
513    /// `IO.Error.otherError`
514    OtherError,
515    /// `IO.Error.resourceBusy`
516    ResourceBusy,
517    /// `IO.Error.resourceVanished`
518    ResourceVanished,
519    /// `IO.Error.unsupportedOperation`
520    UnsupportedOperation,
521    /// `IO.Error.hardwareFault`
522    HardwareFault,
523    /// `IO.Error.unsatisfiedConstraints`
524    UnsatisfiedConstraints,
525    /// `IO.Error.illegalOperation`
526    IllegalOperation,
527    /// `IO.Error.protocolError`
528    ProtocolError,
529    /// `IO.Error.timeExpired`
530    TimeExpired,
531    /// `IO.Error.interrupted`
532    Interrupted,
533    /// `IO.Error.noFileOrDirectory`
534    NoFileOrDirectory,
535    /// `IO.Error.invalidArgument`
536    InvalidArgument,
537    /// `IO.Error.permissionDenied`
538    PermissionDenied,
539    /// `IO.Error.resourceExhausted`
540    ResourceExhausted,
541    /// `IO.Error.inappropriateType`
542    InappropriateType,
543    /// `IO.Error.noSuchThing`
544    NoSuchThing,
545    /// `IO.Error.unexpectedEof`
546    UnexpectedEof,
547    /// `IO.Error.userError`
548    UserError,
549    /// Tag did not match any known `IO.Error` constructor at the active
550    /// Lean toolchain version.
551    Other,
552}
553
554/// Truncate `s` to at most [`LEAN_ERROR_MESSAGE_LIMIT`] bytes on a UTF-8
555/// char boundary. The single place every constructor enforces the bound.
556///
557/// `#[doc(hidden)] pub` so the sibling `lean-rs-host` crate can apply the
558/// same bound when it constructs `LeanError::Host(HostFailure)` values
559/// through the `__host_internals` helpers. Re-exported through
560/// [`crate::__host_internals`]; not part of the public semver promise.
561#[doc(hidden)]
562pub fn bound_message(mut s: String) -> String {
563    if s.len() <= LEAN_ERROR_MESSAGE_LIMIT {
564        return s;
565    }
566    // Walk to the largest char boundary at or below the limit, then
567    // truncate. `floor_char_boundary` is unstable; do it manually with a
568    // single backward scan from the limit. `saturating_sub` keeps clippy's
569    // arithmetic-side-effects lint quiet without changing semantics—the
570    // loop guard already prevents `cut == 0` from underflowing.
571    let mut cut = LEAN_ERROR_MESSAGE_LIMIT;
572    while cut > 0 && !s.is_char_boundary(cut) {
573        cut = cut.saturating_sub(1);
574    }
575    s.truncate(cut);
576    s
577}
578
579// -- Service-layer error helpers --------------------------------------
580//
581// `LeanError`'s constructors are `pub(crate)` to preserve the structural
582// bounding invariant: external crates cannot mint `LeanError` values
583// directly. The sibling `lean-rs-host` crate needs to construct host
584// failures and cooperative cancellation reports when it dispatches
585// capability shims; it reaches the constructors it actually uses through
586// this `#[doc(hidden)] pub fn` wrapper, re-exported at
587// [`crate::__host_internals`].
588//
589// The only wrappers live here are those a real call site needs. Add another the same way
590// (single-call wrapper + re-export in `crate::__host_internals`) only
591// when a future call site needs one.
592
593/// Construct a `ModuleInit` host failure. See [`LeanError::module_init`].
594#[doc(hidden)]
595pub fn host_module_init(message: impl Into<String>) -> LeanError {
596    LeanError::module_init(message)
597}
598
599/// Construct an `Unsupported` host failure.
600#[doc(hidden)]
601pub fn host_unsupported(message: impl Into<String>) -> LeanError {
602    LeanError::host(HostStage::Link, LeanDiagnosticCode::Unsupported, message)
603}
604
605/// Construct a cooperative cancellation report. See [`LeanError::cancelled`].
606#[doc(hidden)]
607pub fn host_cancelled() -> LeanError {
608    LeanError::cancelled()
609}
610
611/// Construct a host-internal failure. See [`LeanError::internal`].
612#[doc(hidden)]
613pub fn host_internal(message: impl Into<String>) -> LeanError {
614    LeanError::internal(message)
615}
616
617/// Construct a host resource-exhaustion failure. See [`LeanError::resource_exhausted`].
618#[doc(hidden)]
619pub fn host_resource_exhausted(message: impl Into<String>) -> LeanError {
620    LeanError::resource_exhausted(message)
621}
622
623/// Construct a host resource-exhaustion failure with structured runtime facts.
624#[doc(hidden)]
625pub fn host_resource_exhausted_with_facts(message: impl Into<String>, facts: ResourceExhaustedFacts) -> LeanError {
626    LeanError::resource_exhausted_with_facts(message, Some(facts))
627}
628
629/// Construct a callback-panic host failure. See [`LeanError::callback_panic`].
630#[doc(hidden)]
631pub fn host_callback_panic(payload: &(dyn Any + Send)) -> LeanError {
632    LeanError::callback_panic(payload)
633}
634
635/// Render an arbitrary panic payload as a human-readable string. Strings
636/// (both `&'static str` and `String`) come through verbatim; other types
637/// collapse to a generic placeholder. Centralised so the
638/// `HostStage::RuntimeInit` and `HostStage::CallbackPanic` sites stay
639/// consistent.
640fn render_panic_payload(payload: &(dyn Any + Send)) -> String {
641    if let Some(s) = payload.downcast_ref::<&'static str>() {
642        (*s).to_owned()
643    } else if let Some(s) = payload.downcast_ref::<String>() {
644        s.clone()
645    } else {
646        "panic payload was not a string".to_owned()
647    }
648}