Struct LeanProgressCallback 

pub struct LeanProgressCallback<'a> { /* private fields */ }

Scoped progress callback registration for one synchronous Lean call.

Unlike LeanCallbackHandle<LeanProgressTick>, the registered closure may borrow from the caller. lean-rs keeps that borrowed context alive until after the callback handle is unregistered, so host crates do not need raw context pointers or stack-lifetime trampolines to report progress.

Lean must not store the (handle, trampoline) pair or invoke it after the synchronous export call has returned. A stale call after drop returns LeanCallbackStatus::StaleHandle, but retaining the values beyond the call violates the scoped callback contract.

Implementations

impl<'a> LeanProgressCallback<'a>

pub fn register<F>(callback: F) -> LeanResult<Self>

where F: Fn(LeanProgressTick) -> LeanCallbackFlow + Send + Sync + 'a,

Register a progress callback whose closure may borrow from the caller.

The returned value must stay alive until Lean can no longer invoke the callback. Dropping it unregisters the handle before releasing the borrowed callback context.

Errors

Returns LeanError::Host with diagnostic code crate::LeanDiagnosticCode::Internal if the callback registry cannot allocate a fresh nonzero id.

pub fn abi_parts(&self) -> (usize, usize)

Return (handle, trampoline) for Lean progress exports using the standard two-USize callback ABI.

pub fn decode_result<'lean, T>(&self, obj: Obj<'lean>) -> LeanResult<T>

where T: TryFromLean<'lean>,

Decode a Lean progress-shim result.

Host progress shims return Except UInt8 T, with Except.ok carrying the real result and Except.error carrying a LeanCallbackStatus byte. This method maps callback panic, stale-handle, wrong-payload, and stop statuses into LeanError while the callback handle is still live, so callers do not need to inspect raw status bytes.

Errors

Returns a conversion error if the object is not a Lean Except UInt8 T shape, or a host error if the callback status reports a contained panic or callback invariant failure.