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}