lean_rs_host/host/
host.rs

1//! `LeanHost`—entry point for the host-side capability API.
2//!
3//! A [`LeanHost`] binds a [`lean_rs::LeanRuntime`] borrow to a Lake project
4//! on disk. From it, [`LeanHost::load_capabilities`] opens a compiled user
5//! capability dylib for its module initializers and imports, while
6//! [`LeanHost::load_shims_only`] opens only the bundled host shims for the
7//! standard session services. Both paths return a [`LeanCapabilities`] whose
8//! sessions resolve checked host-shim bindings once and dispatch subsequent
9//! calls without per-call `dlsym`.
10//!
11//! See `docs/architecture/03-host-stack.md` for the full classification
12//! and the host → capabilities → session lifetime cascade.
13
14use core::fmt;
15use std::path::Path;
16
17use lean_rs::LeanRuntime;
18use lean_rs::error::LeanResult;
19use lean_rs::module::LeanLibrary;
20
21use crate::host::capabilities::LeanCapabilities;
22use crate::host::lake::LakeProject;
23
24/// Entry point for hosting Lean capabilities from a Lake project.
25///
26/// Pairs a runtime borrow with a validated Lake project root. Cheap to
27/// construct: only the project root's existence is checked; no dylib
28/// loading happens until [`LeanHost::load_capabilities`] is called.
29///
30/// Neither [`Send`] nor [`Sync`]: inherited from the contained
31/// `&'lean LeanRuntime`.
32pub struct LeanHost<'lean> {
33    runtime: &'lean LeanRuntime,
34    project: LakeProject,
35}
36
37impl fmt::Debug for LeanHost<'_> {
38    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
39        f.debug_struct("LeanHost").finish_non_exhaustive()
40    }
41}
42
43impl<'lean> LeanHost<'lean> {
44    /// Bind a host to the runtime and a Lake project root directory.
45    ///
46    /// # Errors
47    ///
48    /// Returns [`lean_rs::LeanError::Host`] with stage
49    /// [`lean_rs::HostStage::Load`] if `path` does not exist or is not a
50    /// directory.
51    pub fn from_lake_project(runtime: &'lean LeanRuntime, path: impl AsRef<Path>) -> LeanResult<Self> {
52        let project = LakeProject::new(path)?;
53        Ok(Self { runtime, project })
54    }
55
56    /// Load the compiled capability dylib for the named
57    /// `(package, lib_name)` pair, initialize its root module, and
58    /// prepare the checked host-shim capability used by sessions.
59    ///
60    /// `package` is the Lake package name (e.g. `"lean_rs_fixture"`);
61    /// `lib_name` is the Lake `lean_lib` declaration name and, by
62    /// convention, also the root Lean module path
63    /// (e.g. `"LeanRsFixture"`). For projects where these differ the
64    /// `lib_name` argument is also the module that gets initialised.
65    ///
66    /// # Errors
67    ///
68    /// Returns [`lean_rs::LeanError::Host`] with stage
69    /// [`lean_rs::HostStage::Load`] if the dylib does not exist or fails
70    /// to open. Missing or signature-mismatched mandatory host shims fail when
71    /// constructing a session; optional host shims degrade to `Unsupported` at
72    /// the corresponding call site.
73    pub fn load_capabilities<'h>(&'h self, package: &str, lib_name: &str) -> LeanResult<LeanCapabilities<'lean, 'h>> {
74        let dylib_path = self.project.capability_dylib(package, lib_name);
75        let library = LeanLibrary::open(self.runtime, &dylib_path)?;
76        LeanCapabilities::new(self, library, package, lib_name)
77    }
78
79    /// Load the bundled host-shim and interop dylibs without opening a user
80    /// capability dylib.
81    ///
82    /// Sessions opened from the returned capabilities can import modules from
83    /// this Lake project's `.olean` search path and use the standard
84    /// shim-backed Meta, elaboration, kernel, info-tree, declaration, and
85    /// source-range services.
86    ///
87    /// # Errors
88    ///
89    /// Returns [`lean_rs::LeanError::Host`] with stage
90    /// [`lean_rs::HostStage::Load`] / [`lean_rs::LeanDiagnosticCode::ModuleInit`]
91    /// if the bundled shim or interop dylibs cannot be built or located.
92    /// Returns [`lean_rs::HostStage::Link`] if any mandatory shim symbol is
93    /// missing.
94    pub fn load_shims_only<'h>(&'h self) -> LeanResult<LeanCapabilities<'lean, 'h>> {
95        LeanCapabilities::new_shims_only(self)
96    }
97
98    /// The runtime borrow this host was constructed with.
99    pub(crate) fn runtime(&self) -> &'lean LeanRuntime {
100        self.runtime
101    }
102
103    /// The Lake project root, for capability code that needs to pass
104    /// the path through to Lean (e.g., setting `Lean.searchPathRef`).
105    pub(crate) fn project(&self) -> &LakeProject {
106        &self.project
107    }
108}
lean_rs_host/host/host.rs

lean_rs_host/host/
host.rs
