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 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.

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.