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.

Use LeanWorkerHostHandleBuilder::shims_only for tools that only need the bundled Meta, elaboration, kernel, declaration, and info-tree services. That path does not build or load the user’s :shared facet and therefore keeps working when unrelated user modules break the shared library build.

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 capability Lake project and library.

project_root is the capability project’s directory containing lakefile.lean; it owns the dylib and manifest this builder builds or loads. package is the Lake package name used by lean-rs-host, and lib_name is the Lake lean_lib target to build and load. Session imports default to this same project unless Self::import_workspace_root sets a separate target workspace.

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 capability Lake project root from the standard .lake/build/lib/<dylib> layout. Session imports default to that inferred project unless Self::import_workspace_root sets a separate target workspace. 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 import_workspace_root(self, path: impl Into<PathBuf>) -> Self

Use a separate target Lake workspace root for session imports.

The capability dylib and manifest still come from this builder’s capability project. This root is the single target workspace whose own .lake/build/lib/lean entry and lake-manifest.json dependency closure the worker session imports against. It is not merged with the capability project’s search path.

Tools whose capability project and audited workspace are distinct must set this explicitly. Otherwise the session imports against the capability project, preserving the legacy single-project behavior.

Capability exports that import modules must rely on the host-installed search path. They must not call Lean.initSearchPath or rebuild the search path from LEAN_PATH, because doing so resets Lean’s search path and discards this target workspace root.

pub fn import_profile(self, profile: LeanWorkerSessionImportProfile) -> Self

Select the full-session import profile used for worker host sessions.

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 shutdown_timeout(self, timeout: Duration) -> Self

Set the maximum time to wait for graceful worker shutdown.

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 rss_hard_limit(self, limit_kib: u64, sample_interval: Duration) -> Self

Configure the parent-side hard RSS kill watchdog for in-flight worker requests.

pub fn module_cache_limits(self, limits: LeanWorkerModuleCacheLimits) -> Self

Set typed limits for the worker child’s module snapshot cache.

These are deliberately not exposed as a generic child-env passthrough: the cache knobs are part of the worker lifecycle contract, and callers should not need to know the child process’s environment-variable names.

pub fn num_threads(self, threads: u32) -> Self

Cap the worker child’s Lean task-manager thread pool via LEAN_RS_NUM_THREADS.

Each worker child otherwise starts one task-manager worker thread per hardware core. When several children run, or a single elaboration is memory-heavy, that thread pool multiplies memory pressure. This is a typed knob (not a generic child-env passthrough): callers set a thread count without knowing the child’s environment-variable names.

pub fn lean_max_memory_kib(self, limit_kib: u64) -> Self

Set an opt-in Lean runtime memory ceiling for the worker child via LEAN_RS_LEAN_MAX_MEMORY_KIB.

Lean checks this ceiling periodically and throws before the OS OOM-kills the process, converting a runaway elaboration into a recoverable error instead of a machine crash.

pub fn max_frame_bytes(self, max_frame_bytes: u32) -> Self

Set the per-frame byte cap negotiated with the worker child at handshake.

See LeanWorkerConfig::max_frame_bytes for the policy and the [MIN_FRAME_BYTES, MAX_FRAME_BYTES_HARD_CAP] clamp. Raise this for capabilities whose single logical result composes into one frame (e.g. an outline of an entire module, a file-scoped diagnostics snapshot) and would otherwise trip FrameTooLarge.

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 metadata_export(self, export: impl Into<String>) -> Self

Trust one manifest-backed metadata export with ABI String -> IO String.

pub fn doctor_export(self, export: impl Into<String>) -> Self

Trust one manifest-backed doctor export with ABI String -> IO String.

pub fn json_command_export(self, export: impl Into<String>) -> Self

Trust one manifest-backed JSON command export with ABI String -> IO String.

pub fn streaming_command_export(self, export: impl Into<String>) -> Self

Trust one manifest-backed streaming command export with ABI String, USize, USize -> IO UInt8.

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.