Struct LeanCancellationToken 

pub struct LeanCancellationToken { /* private fields */ }

Shared cooperative cancellation token for LeanSession calls.

LeanCancellationToken is Clone + Send + Sync, so a coordinator thread can keep one clone and the Lean-bound worker thread can pass another clone by reference to session methods. Cancelling sets one atomic bit. Session methods check that bit before FFI dispatches and, for token-aware bulk paths, between per-item dispatches.

This is not pre-emptive cancellation. It does not interrupt an in-flight Lean call. In particular, it cannot stop one stuck isDefEq, a C-side kernel reduction that does not check heartbeats, or an @[export] symbol that runs its own long loop without returning to a lean-rs-host check point. Bound those workloads with Lean heartbeat options, caller-level timeouts, or a worker-process boundary.

use std::thread;
use lean_rs_host::LeanCancellationToken;

let token = LeanCancellationToken::new();
let canceller = token.clone();

thread::spawn(move || {
    // A UI event, request timeout, or supervisor decision would live here.
    canceller.cancel();
});

// On the Lean worker thread:
// session.query_declarations_bulk(&names, Some(&token), None)?;

Implementations

impl LeanCancellationToken

pub fn new() -> Self

Create a token in the non-cancelled state.

pub fn cancel(&self)

Mark this token as cancelled.

Cancellation is one-way. Create a fresh token for a later operation.

pub fn is_cancelled(&self) -> bool

Whether cancellation has been requested.

Trait Implementations

impl Clone for LeanCancellationToken

fn clone(&self) -> LeanCancellationToken

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LeanCancellationToken

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for LeanCancellationToken

fn default() -> LeanCancellationToken

Returns the “default value” for a type.