lean_rs_host/host/
progress.rs

1//! Structured progress reporting for host-session operations.
2//!
3//! Progress is host policy layered over the `lean-rs` scoped progress
4//! callback. Public callers provide a borrowed [`LeanProgressSink`]; this
5//! module maps Lean progress ticks into host phases and elapsed time.
6
7use std::panic::{AssertUnwindSafe, catch_unwind};
8use std::time::{Duration, Instant};
9
10use lean_rs::abi::traits::TryFromLean;
11use lean_rs::{LeanCallbackFlow, LeanProgressCallback, LeanResult, Obj};
12
13/// One structured progress observation from a `LeanSession` operation.
14///
15/// Events are delivered synchronously on the Lean-bound worker thread.
16/// `current` is phase-local and monotonically non-decreasing within one
17/// `phase`. `total = None` means the operation can report a phase-local
18/// counter but does not know the final bound cheaply.
19#[derive(Clone, Copy, Debug, Eq, PartialEq)]
20pub struct LeanProgressEvent {
21    /// Stable phase label for the current operation.
22    pub phase: &'static str,
23    /// Phase-local progress counter.
24    pub current: u64,
25    /// Optional phase-local total.
26    pub total: Option<u64>,
27    /// Time elapsed since this phase started.
28    pub elapsed: Duration,
29}
30
31/// Sink for structured host progress events.
32///
33/// A sink is a one-way callback. It runs synchronously on the thread
34/// currently executing the `LeanSession` method and must not call back
35/// into the same session or re-enter the same Lean call stack. Expensive
36/// work should be queued elsewhere by the sink because progress may be
37/// reported many times for bulk operations.
38///
39/// Rust panics from sinks invoked through Lean progress shims are
40/// contained by the `lean-rs` callback trampoline and returned as a host
41/// internal error. Panics from host-side progress checkpoints are caught
42/// before they escape the session method.
43pub trait LeanProgressSink: Send + Sync {
44    /// Receive one progress event.
45    fn report(&self, event: LeanProgressEvent);
46}
47
48pub(crate) struct ProgressBridge<'a> {
49    callback: LeanProgressCallback<'a>,
50}
51
52impl<'a> ProgressBridge<'a> {
53    pub(crate) fn new(sink: &'a dyn LeanProgressSink, phase: &'static str, total: Option<u64>) -> LeanResult<Self> {
54        let started = Instant::now();
55        let callback = LeanProgressCallback::register(move |event| {
56            sink.report(LeanProgressEvent {
57                phase,
58                current: event.current,
59                total,
60                elapsed: started.elapsed(),
61            });
62            LeanCallbackFlow::Continue
63        })?;
64        Ok(Self { callback })
65    }
66
67    pub(crate) fn abi_parts(&self) -> (usize, usize) {
68        self.callback.abi_parts()
69    }
70
71    pub(crate) fn decode<'lean, T>(&self, obj: Obj<'lean>) -> LeanResult<T>
72    where
73        T: TryFromLean<'lean>,
74    {
75        self.callback.decode_result(obj)
76    }
77}
78
79pub(crate) fn report_progress(
80    sink: Option<&dyn LeanProgressSink>,
81    phase: &'static str,
82    current: u64,
83    total: Option<u64>,
84    started: Instant,
85) -> LeanResult<()> {
86    let Some(sink) = sink else {
87        return Ok(());
88    };
89    let event = LeanProgressEvent {
90        phase,
91        current,
92        total,
93        elapsed: started.elapsed(),
94    };
95    catch_unwind(AssertUnwindSafe(|| sink.report(event)))
96        .map_err(|payload| lean_rs::__host_internals::host_callback_panic(payload.as_ref()))
97}
lean_rs_host/host/progress.rs

lean_rs_host/host/
progress.rs
