Struct LeanCapabilities 

pub struct LeanCapabilities<'lean, 'h> { /* private fields */ }

Loaded generic interop, host shim, and optional user dylibs with a checked host-shim capability ready for session binding resolution.

Owns the LeanLibrary handles so callers do not have to track the dylibs’ lifetimes separately. Borrows from the parent LeanHost for the runtime + project context. Neither Send nor Sync: inherited from the contained LeanLibrary handles.

Implementations

impl<'lean, 'h> LeanCapabilities<'lean, 'h>

pub fn session<'c>( &'c self, imports: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<LeanSession<'lean, 'c>>

Import the named modules into a fresh Lean environment and return a session over the result.

Imports happen exactly once per session() call. The returned LeanSession owns the imported environment and reuses this capability’s checked shim bindings for every query.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before import dispatch.

Returns lean_rs::LeanError::LeanException if the Lean-side import raises (missing .olean, malformed module name, …), with the bounded message Lean surfaced.

pub fn session_with_profile<'c>( &'c self, imports: &[&str], profile: LeanSessionImportProfile, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<LeanSession<'lean, 'c>>

Import using an explicit full-session import profile.

Use this when a caller intentionally needs a broader import shape than the default private profile. No profile falls back silently to another one: import and service failures are reported for the requested profile.

Errors

Returns a host resource error when same-process cargo-test imports are blocked, a cancellation error when cancellation is already cancelled, or the Lean/import failure surfaced by the requested profile.

pub fn profiling_session<'c>( &'c self, imports: &[&str], mode: LeanImportProfileMode, profiler_options: &LeanImportProfilerOptions, ) -> LeanResult<LeanSession<'lean, 'c>>

Import using one of the closed diagnostic import modes.

This exists for profiling import breadth only. Normal host sessions use Self::session, whose default is LeanSessionImportProfile::Private.

Errors

Returns a host resource error when same-process cargo-test imports are blocked, or the Lean/import failure surfaced by the requested diagnostic mode.

pub fn bracketed_import_query( &self, imports: &[&str], request: LeanBracketedImportRequest, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<LeanBracketedImportResult>

Run a one-shot no-extension import query inside Lean’s compacted-region bracket.

The Lean shim uses withImportModules, which imports with loadExts := false, serializes only the requested declaration metadata plus import stats, frees the imported compacted regions, and then returns Rust-owned data. It is deliberately not a replacement for Self::session: parser, elaboration, proof-state, pretty-printing, and capability workflows require full sessions with loaded extensions. Extending this path to return Lean-owned objects would be unsound unless their lifetime across Environment.freeRegions can be proven locally.

Errors

Returns the Lean/import or ABI-conversion failure encountered while running the closed bracketed query.

Trait Implementations

impl Debug for LeanCapabilities<'_, '_>

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

Formats the value using the given formatter.