Struct LeanWorkerCapability 

pub struct LeanWorkerCapability { /* private fields */ }

A worker-backed capability with its Lake target built and worker started.

The value owns the worker supervisor and the session configuration. It is the normal entry point for downstream capability use until the typed command facade lands on top of it.

Implementations

impl LeanWorkerCapability

pub fn open_session( &mut self, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerSession<'_>, LeanWorkerError>

Open a worker session for this capability.

The builder has already proved that the session can open. This method is still fallible because worker cycling, cancellation, or a child failure may require a fresh session.

Errors

Returns LeanWorkerError if the worker is dead, the child cannot open the configured imports, cancellation is already requested, a progress sink panics, or protocol communication fails.

pub fn dylib_path(&self) -> &Path

Return the built capability dylib path resolved by lean-toolchain.

pub fn session_config(&self) -> &LeanWorkerSessionConfig

Return the session configuration used by this capability.

pub fn validated_metadata(&self) -> Option<&LeanWorkerCapabilityMetadata>

Return capability metadata validated by the builder, if requested.

pub fn runtime_metadata(&self) -> LeanWorkerRuntimeMetadata

Return protocol/runtime facts captured from the worker handshake.

pub fn worker(&self) -> &LeanWorker

Borrow the underlying worker for lifecycle operations such as cycling.

pub fn worker_mut(&mut self) -> &mut LeanWorker

Mutably borrow the underlying worker for lifecycle operations such as cycling.

pub fn terminate(self) -> Result<LeanWorkerExit, LeanWorkerError>

Terminate the worker child and return its exit status.

Errors

Returns LeanWorkerError if the worker is already dead, the terminate request fails, or waiting for the child fails.

Trait Implementations

impl Debug for LeanWorkerCapability

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

Formats the value using the given formatter.