lean_rs_host/host/process/outcome.rs
1//! [`ProcessFileOutcome`] — the typed outcome of
2//! [`crate::LeanSession::process_with_info_tree`].
3//!
4//! Two branches cover the cases callers must distinguish:
5//!
6//! - `Processed` — the elaborator ran; the projection is in the
7//! payload. Heartbeat exhaustion during a single command's
8//! elaboration surfaces as an error-severity entry in
9//! `ProcessedFile::diagnostics`, the same path the elaborator uses
10//! for any other failed command — there is no separate "timed out"
11//! wire arm because `IO.processCommands` catches per-command
12//! exceptions and attaches them to the message log.
13//! - `Unsupported` — the loaded capability dylib does not export
14//! `lean_rs_host_process_with_info_tree`. The session returns this
15//! without invoking the FFI, matching the meta-service degradation
16//! pattern.
17
18use crate::host::process::info_tree::ProcessedFile;
19
20/// Outcome of [`crate::LeanSession::process_with_info_tree`].
21///
22/// `#[non_exhaustive]` so future capability refinements can extend the
23/// taxonomy without breaking exhaustive matches.
24#[derive(Debug)]
25#[non_exhaustive]
26pub enum ProcessFileOutcome {
27 /// The elaborator ran and produced an `Elab.InfoTree` projection.
28 /// `ProcessedFile::diagnostics` carries every error-severity entry
29 /// the elaborator emitted; callers that need to distinguish
30 /// heartbeat exhaustion from other failures should match on the
31 /// diagnostics there.
32 Processed(ProcessedFile),
33 /// The capability dylib does not export the
34 /// `lean_rs_host_process_with_info_tree` shim. No FFI call was
35 /// made; callers can fall back or degrade as appropriate.
36 Unsupported,
37}