Struct LeanWorkerConfig 

pub struct LeanWorkerConfig { /* private fields */ }

Configuration for starting a lean-rs-worker child process.

The executable should be the lean-rs-worker-child binary.

Worker-child panic policy. The supervisor spawns every child with two defaults that together pin a process boundary around Lean panics:

• LEAN_ABORT_ON_PANIC=1—Lean internal panics terminate the child instead of returning default values, so the parent observes a fatal exit rather than silently-corrupted state.
• LEAN_BACKTRACE=0—Lean’s panic-time backtrace handler is skipped. Since Lean 4.30 that handler calls back into Lean code (the demangler is now @[export]’d from Lean.Compiler.NameDemangling); a worker child embeds a minimal Lean and cannot guarantee that callback’s transitive module dependencies are initialized when user code panics. Disabling the backtrace removes that dependency entirely. See docs/architecture/06-panic-containment.md for the boundary argument.

Both are safe defaults—explicit .env() entries supplied here override them, in case a caller knows the dependency is satisfied and wants a demangled backtrace on the child’s stderr.

Implementations

impl LeanWorkerConfig

pub fn new(executable: impl Into<PathBuf>) -> Self

Create a worker configuration for a child executable.

pub fn executable(&self) -> &Path

Return the child executable path.

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

Set the child working directory.

pub fn env(self, key: impl Into<OsString>, value: impl Into<OsString>) -> Self

Add or override one child environment variable.

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

Set the maximum time to wait for the child handshake.

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

Set the maximum time to wait for one request’s terminal response.

The request timeout starts after the request frame is written. It covers live rows, diagnostics, progress events, and the terminal response. On timeout, the supervisor kills and replaces the child process.

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

Set the maximum time to wait for graceful worker shutdown.

Explicit shutdown and Drop both ask the child to terminate first. If this deadline expires before the child exits, the supervisor kills the process and waits for it to be reaped.

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.

Policy checks run before requests enter the child. A policy restart is a process restart; it is the only supported reset for Lean process-global runtime and import state.

pub fn rss_hard_limit(self, limit_kib: u64, sample_interval: Duration) -> Self

Kill and replace the worker during an in-flight request if its RSS is sampled at or above limit_kib.

This is a protective hard stop, not a throughput optimization. The request that crosses the limit returns LeanWorkerError::RssHardLimitExceeded after the child is replaced.

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

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

The cap is announced to the child immediately after its handshake frame and applies in both directions for the lifetime of the connection. The default is MAX_FRAME_BYTES (1 MiB), which is enough for every session-backed tool whose result composes from many frames. Capabilities whose single logical result is a frame—e.g. an outline of an entire module, or a diagnostics snapshot of a refactor-in-progress file—can raise the cap here to admit larger envelopes.

Values are clamped into [MIN_FRAME_BYTES, MAX_FRAME_BYTES_HARD_CAP]. The floor keeps even a malformed setter from breaking the handshake itself; the ceiling prevents the memory-safety policy from being defeated by an absurd value.

Trait Implementations

impl Clone for LeanWorkerConfig

fn clone(&self) -> LeanWorkerConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerConfig

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

Formats the value using the given formatter.