lean_rs_host/host/
cancellation.rs

1//! Cooperative cancellation for long-running session operations.
2//!
3//! The token is deliberately just one atomic bit. Policy stays with the
4//! caller: UI code, request handlers, or worker supervisors decide when to
5//! flip the bit; `lean-rs-host` only checks it at documented boundaries.
6
7use std::sync::Arc;
8use std::sync::atomic::{AtomicBool, Ordering};
9
10use lean_rs::LeanResult;
11
12/// Shared cooperative cancellation token for `LeanSession` calls.
13///
14/// `LeanCancellationToken` is `Clone + Send + Sync`, so a coordinator
15/// thread can keep one clone and the Lean-bound worker thread can pass
16/// another clone by reference to session methods. Cancelling sets one
17/// atomic bit. Session methods check that bit before FFI dispatches and,
18/// for token-aware bulk paths, between per-item dispatches.
19///
20/// This is not pre-emptive cancellation. It does **not** interrupt an
21/// in-flight Lean call. In particular, it cannot stop one stuck `isDefEq`,
22/// a C-side kernel reduction that does not check heartbeats, or an
23/// `@[export]` symbol that runs its own long loop without returning to a
24/// `lean-rs-host` check point. Bound those workloads with Lean heartbeat
25/// options, caller-level timeouts, or a worker-process boundary.
26///
27/// ```no_run
28/// use std::thread;
29/// use lean_rs_host::LeanCancellationToken;
30///
31/// let token = LeanCancellationToken::new();
32/// let canceller = token.clone();
33///
34/// thread::spawn(move || {
35///     // A UI event, request timeout, or supervisor decision would live here.
36///     canceller.cancel();
37/// });
38///
39/// // On the Lean worker thread:
40/// // session.query_declarations_bulk(&names, Some(&token), None)?;
41/// # let _ = token;
42/// ```
43#[derive(Clone, Debug, Default)]
44pub struct LeanCancellationToken {
45    cancelled: Arc<AtomicBool>,
46}
47
48impl LeanCancellationToken {
49    /// Create a token in the non-cancelled state.
50    #[must_use]
51    pub fn new() -> Self {
52        Self::default()
53    }
54
55    /// Mark this token as cancelled.
56    ///
57    /// Cancellation is one-way. Create a fresh token for a later operation.
58    pub fn cancel(&self) {
59        self.cancelled.store(true, Ordering::Release);
60    }
61
62    /// Whether cancellation has been requested.
63    #[must_use]
64    pub fn is_cancelled(&self) -> bool {
65        self.cancelled.load(Ordering::Acquire)
66    }
67}
68
69pub(crate) fn check_cancellation(token: Option<&LeanCancellationToken>) -> LeanResult<()> {
70    if token.is_some_and(LeanCancellationToken::is_cancelled) {
71        return Err(lean_rs::__host_internals::host_cancelled());
72    }
73    Ok(())
74}
lean_rs_host/host/cancellation.rs

lean_rs_host/host/
cancellation.rs
