Struct LeanWorkerCapabilityBuilder 

pub struct LeanWorkerCapabilityBuilder { /* private fields */ }

Builder for a worker-backed Lean capability session.

The builder hides the common setup sequence for downstream tools:

1. build the Lake shared-library target with lean-toolchain;
2. resolve and start the lean-rs-worker-child process;
3. health-check the worker;
4. open the configured host session once; and
5. optionally validate downstream capability metadata.

Callers still provide the Lake project root, package name, library target, and imports because those are the downstream capability’s identity. Worker framing, child lifecycle, path probing, timeouts, and restart policy stay behind the builder.

Implementations

impl LeanWorkerCapabilityBuilder

pub fn new( project_root: impl Into<PathBuf>, package: impl Into<String>, lib_name: impl Into<String>, imports: impl IntoIterator<Item = impl Into<String>>, ) -> Self

Create a builder for a Lake project and capability library.

project_root is the directory containing lakefile.lean. package is the Lake package name used by lean-rs-host, and lib_name is the Lake lean_lib target to build and load.

pub fn from_built_capability( spec: &LeanBuiltCapability, imports: impl IntoIterator<Item = impl Into<String>>, ) -> Result<Self, LeanWorkerError>

Create a builder from a build-script produced capability.

Manifest-backed descriptors are the canonical packaged-app path. The builder reads package, module, and primary dylib facts from the manifest, then infers the Lake project root from the standard .lake/build/lib/<dylib> layout so the worker child can initialize Lean’s import search path. Direct dylib descriptors remain supported as a compatibility path when callers also provide package and module names.

Errors

Returns LeanWorkerError if manifest data cannot be parsed, the fallback dylib path cannot be resolved, the compatibility descriptor is missing package/module names, or the dylib is not under a standard Lake build directory.

pub fn worker_executable(self, path: impl Into<PathBuf>) -> Self

Use an explicit lean-rs-worker-child executable.

Tests and packaged applications should use this when the worker child is not discoverable beside the current executable.

pub fn worker_child(self, child: LeanWorkerChild) -> Self

Resolve the worker executable with a packaged worker-child locator.

pub fn startup_timeout(self, timeout: Duration) -> Self

Set the maximum time to wait for worker startup.

pub fn request_timeout(self, timeout: Duration) -> Self

Set the maximum time to wait for one worker request.

pub fn long_running_requests(self) -> Self

Use the documented long-running request timeout profile.

pub fn restart_policy(self, policy: LeanWorkerRestartPolicy) -> Self

Set the worker restart policy used after startup.

pub fn validate_metadata( self, export: impl Into<String>, request: Value, ) -> Self

Validate generic capability metadata after the session opens.

The export must have ABI String -> IO String, matching LeanWorkerSession::capability_metadata. The returned metadata is stored on the opened capability for callers that need it.

pub fn expect_metadata( self, export: impl Into<String>, request: Value, expected: LeanWorkerCapabilityMetadata, ) -> Self

Validate that a capability metadata export returns the expected facts.

This is the pool-facing metadata expectation hook. The metadata remains downstream-defined; lean-rs-worker only checks that the generic metadata envelope matches the caller’s requested expectation.

pub fn session_key(&self) -> LeanWorkerSessionKey

Return the session reuse key represented by this builder.

The key is for worker-pool reuse only. It is not a downstream cache key and does not encode row schemas, ranking, reporting, or source provenance.

pub fn check(&self) -> LeanWorkerBootstrapReport

Check deployment facts before running a real worker command.

The report validates the worker child locator, manifest-backed capability artifact when present, worker protocol handshake, session opening, and optional metadata expectation. It keeps child paths, protocol frames, and loader environment details below the worker boundary.

pub fn open(self) -> Result<LeanWorkerCapability, LeanWorkerError>

Build the Lake target, start the worker, open the session, and return a ready capability.

Errors

Returns LeanWorkerError if Lake cannot build the target, the worker child cannot be resolved or spawned, the worker fails startup/health, the session cannot open, or metadata validation fails.

Trait Implementations

impl Clone for LeanWorkerCapabilityBuilder

fn clone(&self) -> LeanWorkerCapabilityBuilder

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerCapabilityBuilder

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

Formats the value using the given formatter.