Struct LeanWorkerChild 

pub struct LeanWorkerChild { /* private fields */ }

Locator for an app-owned worker child executable.

Dependency binaries are not automatically installed with downstream applications. Production apps should ship a tiny binary that calls lean_rs_worker_child::run_worker_child_stdio and point the capability builder at it through this locator.

Toolchain binding

A worker child binary is built against one Lean toolchain: its rpath points at one libleanshared, and LEAN_SYSROOT at spawn time must point at the matching stdlib oleans (<sysroot>/lib/lean/Init.olean). Mismatched rpath and sysroot abort with incompatible header before the handshake.

The locator carries both: the binary path (via Self::path or Self::sibling) and, optionally, the matching sysroot (via Self::for_toolchain or Self::lean_sysroot). When the supervisor spawns the child, it sets LEAN_SYSROOT from the locator (or from lean_toolchain::discover_toolchain as a fallback) so callers never have to thread the env var manually.

Design note: no generic env(key, value) passthrough

LeanWorkerCapabilityBuilder and LeanWorkerChild deliberately do not expose a general env(key, value) builder. Every environment variable the worker child cares about has a typed method whose name describes the invariant it enforces (e.g. Self::lean_sysroot enforces the rpath/sysroot match). If a future env var needs to be plumbed through, add a typed builder for it — do not add a generic env(...). Generic passthroughs leak implementation knowledge (env var names, framing invariants) into every caller and erode the structural guarantee that supported configurations cannot be misconstructed.

Implementations

impl LeanWorkerChild

pub fn sibling(executable_name: impl Into<String>) -> Self

Locate a worker child beside the current executable, or beside the Cargo profile directory during tests and cargo run.

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

Use an explicit worker child path.

pub fn for_toolchain( path: impl Into<PathBuf>, sysroot: impl Into<PathBuf>, ) -> Self

Locate a worker child and declare the Lean toolchain its rpath was built against.

sysroot is the Lean prefix containing lib/lean/Init.olean. The supervisor sets LEAN_SYSROOT to this value when spawning the child, so a single parent process can host multiple workers each pinned to a different toolchain.

pub fn lean_sysroot(self, sysroot: impl Into<PathBuf>) -> Self

Set or override the Lean sysroot the spawned child uses.

When unset, the supervisor falls back to lean_toolchain::discover_toolchain at spawn time.

pub fn env_override(self, env_var: impl Into<String>) -> Self

Add an environment-variable override for launchers and tests.

Trait Implementations

impl Clone for LeanWorkerChild

fn clone(&self) -> LeanWorkerChild

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerChild

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

Formats the value using the given formatter.

impl Default for LeanWorkerChild

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq for LeanWorkerChild

fn eq(&self, other: &LeanWorkerChild) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for LeanWorkerChild

impl StructuralPartialEq for LeanWorkerChild