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.

Provisioning is the caller’s job

This locator only finds a worker child; it does not install one. Dependency binaries are not shipped with downstream applications, so a downstream must provision its own worker child — ship it beside the host binary (resolved by Self::sibling), point at it explicitly (Self::path / Self::for_toolchain), or supply it through an Self::env_override variable. The one exception is a developer convenience internal to the lean-rs source tree: when the requested name is the default lean-rs-worker-child and resolution runs from within the lean-rs workspace, Self::sibling also falls back to building that binary with cargo build -p lean-rs-worker-child (so the workspace’s own examples and profiling harness run with no extra steps). That fallback is keyed to lean-rs’s own CARGO_MANIFEST_DIR and is inert for every downstream — outside the source tree it finds no workspace to build and no-ops. Do not rely on it from a consuming crate.

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.

For the default name lean-rs-worker-child, resolution additionally falls back to building the binary from source — but only inside the lean-rs workspace itself. See the type-level provisioning note: that fallback is an in-tree developer convenience and is inert for downstream callers, which must ship or point at their own worker child.

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 Eq for LeanWorkerChild

impl PartialEq for LeanWorkerChild

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LeanWorkerChild