lean_rs/module/
bundle.rs

1//! Capability-level loader that anchors dependent Lean libraries.
2//!
3//! [`LeanLibrary`] is intentionally low-level: it owns one dynamic-loader
4//! handle. [`LeanLibraryBundle`] is the shipped-capability boundary. It opens
5//! dependency dylibs first, gives them exported symbol visibility when a later
6//! Lean dylib needs it, initializes dependency modules when requested, and keeps
7//! every handle alive until the primary capability is dropped.
8
9use std::path::Path;
10
11use super::{LeanLibrary, LeanModule};
12use crate::error::LeanResult;
13use crate::runtime::LeanRuntime;
14
15// `LeanLibraryDependency` and `LeanModuleInitializer` are pure data shared
16// with the worker wire protocol; they live in `lean-toolchain` (below
17// `lean-rs`) so the protocol crate can reference them without re-linking
18// `libleanshared`. Re-exported here for callers using the historical paths.
19pub use lean_toolchain::{LeanLibraryDependency, LeanModuleInitializer};
20
21/// A primary Lean capability plus its dependent Lean dylibs.
22///
23/// The primary library is dropped before dependency libraries so imported
24/// symbols remain available for as long as capability code can run.
25pub struct LeanLibraryBundle<'lean> {
26    primary: LeanLibrary<'lean>,
27    dependencies: Vec<LeanLibrary<'lean>>,
28}
29
30impl<'lean> LeanLibraryBundle<'lean> {
31    /// Open a primary capability dylib and every dependency it needs.
32    ///
33    /// Dependencies are opened and optionally initialized in iterator order.
34    /// The primary dylib is opened last. Every dependency handle is stored
35    /// inside the bundle, so helper functions can return a bundle without
36    /// leaking handles or relying on platform loader state that outlives Rust's
37    /// RAII values.
38    ///
39    /// # Errors
40    ///
41    /// Returns [`crate::LeanError`] if any dependency or primary dylib cannot
42    /// be opened, or if any requested dependency initializer fails.
43    pub fn open(
44        runtime: &'lean LeanRuntime,
45        primary_path: impl AsRef<Path>,
46        dependencies: impl IntoIterator<Item = LeanLibraryDependency>,
47    ) -> LeanResult<Self> {
48        let mut opened_dependencies = Vec::new();
49        for dependency in dependencies {
50            let library = if dependency.exports_symbols_for_dependents() {
51                LeanLibrary::open_globally(runtime, dependency.path_ref())?
52            } else {
53                LeanLibrary::open(runtime, dependency.path_ref())?
54            };
55            if let Some(initializer) = dependency.into_module_initializer() {
56                let _module = library.initialize_module(initializer.package_name(), initializer.module_name())?;
57            }
58            opened_dependencies.push(library);
59        }
60
61        let primary = LeanLibrary::open(runtime, primary_path)?;
62        Ok(Self {
63            primary,
64            dependencies: opened_dependencies,
65        })
66    }
67
68    /// Initialize a module from the primary capability library.
69    ///
70    /// This delegates to [`LeanLibrary::initialize_module`] while preserving the
71    /// bundle lifetime that keeps dependent dylibs anchored.
72    ///
73    /// # Errors
74    ///
75    /// Returns [`crate::LeanError`] if the requested module name cannot be
76    /// mapped to an initializer symbol, if that symbol is missing from the
77    /// primary library, or if the Lean initializer returns `IO.error`.
78    pub fn initialize_module<'bundle>(
79        &'bundle self,
80        package: &str,
81        module: &str,
82    ) -> LeanResult<LeanModule<'lean, 'bundle>> {
83        self.primary.initialize_module(package, module)
84    }
85
86    /// Borrow the primary capability library.
87    #[must_use]
88    pub fn library(&self) -> &LeanLibrary<'lean> {
89        &self.primary
90    }
91
92    /// Number of dependency dylibs anchored by this bundle.
93    #[must_use]
94    pub fn dependency_count(&self) -> usize {
95        self.dependencies.len()
96    }
97}
98
99impl std::fmt::Debug for LeanLibraryBundle<'_> {
100    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
101        f.debug_struct("LeanLibraryBundle")
102            .field("primary", &self.primary)
103            .field("dependency_count", &self.dependencies.len())
104            .finish()
105    }
106}
lean_rs/module/bundle.rs

lean_rs/module/
bundle.rs
