Struct LeanLakeProjectModules 

pub struct LeanLakeProjectModules {
    pub requested_root: PathBuf,
    pub project_root: PathBuf,
    pub lakefile: PathBuf,
    pub declared_lean_libs: Vec<String>,
    pub module_roots: Vec<String>,
    pub selected_roots: Vec<String>,
    pub modules: Vec<LeanModuleDescriptor>,
    pub fingerprint: LeanModuleSetFingerprint,
}

A discovered Lake project and its Lean modules.

Fields

requested_root: PathBuf

project_root: PathBuf

lakefile: PathBuf

declared_lean_libs: Vec<String>

Lakefile-declared lean_lib target names, in lexicographic order.

Empty when the lakefile declares no lean_lib targets. Distinct from module_roots, which falls back to discovering top-level *.lean files when no declaration is found. Callers verifying that a build target was explicitly declared must consult this field, not module_roots.

module_roots: Vec<String>

selected_roots: Vec<String>

modules: Vec<LeanModuleDescriptor>

fingerprint: LeanModuleSetFingerprint

Trait Implementations

impl Clone for LeanLakeProjectModules

fn clone(&self) -> LeanLakeProjectModules

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanLakeProjectModules

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

Formats the value using the given formatter.

impl PartialEq for LeanLakeProjectModules

fn eq(&self, other: &LeanLakeProjectModules) -> 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 LeanLakeProjectModules

impl StructuralPartialEq for LeanLakeProjectModules