Struct LeanThreadGuard 

pub struct LeanThreadGuard<'lean> { /* private fields */ }

RAII handle that attaches the current OS thread to the Lean runtime.

When constructed via LeanThreadGuard::attach, the guard registers the calling thread with the Lean runtime so that thread may invoke compiled Lean code. When the guard is dropped (or its scope ends), the thread is detached again. Threads spawned by Lean itself are already attached and do not need a guard; the thread that called crate::LeanRuntime::init is likewise treated as attached for its entire lifetime.

The guard is neither Send nor Sync: it represents a per-thread resource, and shipping it to a different OS thread to be dropped would detach the wrong thread. The 'lean lifetime parameter ties the guard to a LeanRuntime borrow, so a guard cannot outlive the runtime it is bound to.

Nested attaches are legal: a worker thread already inside an outer LeanThreadGuard may construct another (e.g. inside a callback) and the per-thread attach depth tracks the pairs so the host-call attach assertion does not fire prematurely.

Example

// Inside a worker thread you spawned yourself:
let runtime = lean_rs::LeanRuntime::init()?;
let _guard = lean_rs::LeanThreadGuard::attach(runtime);
// ... call into Lean from this thread ...
// `_guard` is dropped at scope exit, detaching the thread cleanly.

Implementations

impl<'lean> LeanThreadGuard<'lean>

pub fn attach(_runtime: &'lean LeanRuntime) -> Self

Attach the current OS thread to the Lean runtime.

Construction requires a borrow of the process LeanRuntime handle; that borrow is the type-level proof that the runtime has been initialized on this process. The returned guard must be dropped on the same thread that attached it.

Trait Implementations

impl Drop for LeanThreadGuard<'_>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.