Struct LeanWorkerHostHandleBuilder 

pub struct LeanWorkerHostHandleBuilder { /* private fields */ }

Builder for a worker-backed host session that loads only bundled shims.

This is the bootstrap path for tools that use the standard host services exposed through lean-rs-host: Meta queries, elaboration, kernel checking, declaration listing, source ranges, and info trees. It deliberately has no package/library fields and no metadata validation hook because no user @[export] dylib is built or opened.

Implementations

impl LeanWorkerHostHandleBuilder

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

Create a shims-only worker host-session builder for a Lake project.

project_root is the directory containing lakefile.lean. imports are the modules to import when the builder performs its initial session open. The builder does not build a Lake :shared target.

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

Use an explicit lean-rs-worker-child 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 max_frame_bytes(self, max_frame_bytes: u32) -> Self

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

pub fn check(&self) -> LeanWorkerBootstrapReport

Check worker bootstrap facts before running a real command.

The report validates the worker child locator, protocol handshake, and shims-only session opening. It never builds a user shared-library target.

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

Start the worker, open a shims-only host session once, and return a ready handle.

Errors

Returns LeanWorkerError if the worker child cannot be resolved or spawned, startup/health fails, or the shims-only session cannot open. This method does not build a user Lake shared-library target.

Trait Implementations

impl Clone for LeanWorkerHostHandleBuilder

fn clone(&self) -> LeanWorkerHostHandleBuilder

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerHostHandleBuilder

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

Formats the value using the given formatter.