Struct SessionPool 

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

A capacity-bounded reuse pool of imported Lean environments.

Built with Self::with_capacity; environments enter the pool through PooledSession::drop (returning a previously-acquired session). Pool entries are capability-agnostic: a single pool may be shared across multiple LeanCapabilities values, as long as they share the same runtime.

Neither Send nor Sync (inherited from the contained Obj<'lean> values).

Implementations

impl<'lean> SessionPool<'lean>

pub fn with_capacity(runtime: &'lean LeanRuntime, capacity: usize) -> Self

Build an empty pool with hard upper bound capacity on stored environments.

A capacity of 0 disables reuse — every Self::acquire call imports fresh and every release drops the environment. This is useful for tests that want metrics without recycling, and as the degenerate point that proves the pool’s metrics agree with repeated caps.session(..., None, None) calls.

The runtime borrow witnesses 'lean and is stored so the pool itself outlives every entry on its free list — even after every PooledSession has been dropped, the pool retains a usable runtime reference.

pub fn acquire<'p, 'c>( &'p self, caps: &'c LeanCapabilities<'lean, 'c>, imports: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<PooledSession<'lean, 'p, 'c>>

Acquire a session targeting imports under caps.

If a pooled environment was previously released with the same imports list (order-sensitive), it is rewrapped under the supplied capability borrow and returned — no Lean.importModules runs. Otherwise the pool calls LeanCapabilities::session internally to perform a fresh import. Either way, the resulting PooledSession returns the underlying environment to the pool on Drop.

caps must come from the same LeanRuntime the pool was constructed with; this is structurally enforced by the shared 'lean lifetime parameter.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before the pool can reuse or import an environment.

Returns lean_rs::LeanError::LeanException if a fresh import is required and the Lean-side lean_rs_host_session_import shim raises through IO. Cached environments never re-fail.

pub fn stats(&self) -> PoolStats

Snapshot the accumulated pool metrics.

Counters never reset; subtract two snapshots to measure activity over an interval. See PoolStats for the field invariants (e.g. imports_performed + reused == acquired).

pub fn len(&self) -> usize

Number of environments currently sitting on the free list.

This is the count of warm imports available for the next Self::acquire without going through Lean.importModules. Explicit drains and cache hits both remove entries from this count; releases may add entries back up to Self::capacity.

pub fn is_empty(&self) -> bool

true iff Self::len is zero; every subsequent Self::acquire will perform a fresh import.

pub fn capacity(&self) -> usize

Configured hard upper bound on the free list.

Set by Self::with_capacity. A pool releasing a PooledSession while at capacity drops the environment instead of pushing it back; that release shows up in PoolStats::released_dropped rather than released_to_pool.

pub fn drain(&self) -> usize

Drop every cached environment currently retained by the pool.

Returns the number of free-list entries removed. Each removed entry drops its owned Obj<'lean> environment, which releases one Lean refcount via lean_dec.

Checked-out PooledSession values are not affected: they own their sessions until drop, and may return their environments to this same pool later if capacity permits. A later Self::drain call can remove those returned entries.

This is a cache-eviction API, not a runtime recycle API. It does not reset Lean’s process-global runtime state, initialized module flags, interned names, compacted .olean regions, or allocator arenas, and should not be treated as an RSS reset.

Trait Implementations

impl Debug for SessionPool<'_>

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

Formats the value using the given formatter.