Struct LeanWorkerSessionKey 

pub struct LeanWorkerSessionKey { /* private fields */ }

Worker reuse key for a capability-backed session.

A session key answers only one pool question: can an already-open child session safely host compatible work? The key includes both the capability project root and the import workspace root because one open session has one fixed Lean search path. It is not a downstream cache key, and it does not encode row schemas, cache validity, ranking, reporting, or source provenance.

Implementations

impl LeanWorkerSessionKey

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

Create a session key from the caller-visible capability requirements.

project_root is the capability project root. The import workspace root defaults to the same value; capability builders with a distinct target workspace override it internally.

pub fn metadata_expectation( self, export: impl Into<String>, request: Value, expected: Option<LeanWorkerCapabilityMetadata>, ) -> Self

Add the metadata expectation used to decide safe session reuse.

expected is downstream metadata transported by the generic metadata envelope. The pool compares it as opaque facts and does not interpret command names or semantic versions.

pub fn restart_policy_class(self, class: LeanWorkerRestartPolicyClass) -> Self

Set the coarse restart-policy class for this session key.

pub fn project_root(&self) -> &Path

Return the capability Lake project root for this session key.

pub fn import_workspace_root(&self) -> &Path

Return the target Lake workspace root whose dependency closure the session imports against.

pub fn package(&self) -> &str

Return the Lake package name for this session key.

pub fn lib_name(&self) -> &str

Return the Lake library target for this session key.

pub fn imports(&self) -> &[String]

Return the imports required by this session key.

pub fn import_profile(&self) -> LeanWorkerSessionImportProfile

Return the import profile required by this session key.

pub fn toolchain_fingerprint(&self) -> &ToolchainFingerprint

Return the build-baked Lean toolchain fingerprint used by this key.

pub fn policy_class(&self) -> LeanWorkerRestartPolicyClass

Return the restart-policy class used by this key.

Trait Implementations

impl Clone for LeanWorkerSessionKey

fn clone(&self) -> LeanWorkerSessionKey

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerSessionKey

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

Formats the value using the given formatter.

impl Eq for LeanWorkerSessionKey

impl PartialEq for LeanWorkerSessionKey

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LeanWorkerSessionKey