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
5//! capability dylib (e.g. `liblean__rs__fixture_LeanRsFixture.dylib`),
6//! pre-resolves the capability's session symbol addresses, and returns
7//! a [`LeanCapabilities`] that subsequent calls dispatch through without
8//! per-call `dlsym`.
9//!
10//! See `docs/architecture/03-host-stack.md` for the full classification
11//! and the host → capabilities → session lifetime cascade.
12
13use core::fmt;
14use std::path::Path;
15
16use crate::host::capabilities::LeanCapabilities;
17use crate::host::lake::LakeProject;
18use lean_rs::LeanRuntime;
19use lean_rs::error::LeanResult;
20use lean_rs::module::LeanLibrary;
21
22/// Entry point for hosting Lean capabilities from a Lake project.
23///
24/// Pairs a runtime borrow with a validated Lake project root. Cheap to
25/// construct: only the project root's existence is checked; no dylib
26/// loading happens until [`LeanHost::load_capabilities`] is called.
27///
28/// Neither [`Send`] nor [`Sync`]: inherited from the contained
29/// `&'lean LeanRuntime`.
30pub struct LeanHost<'lean> {
31    runtime: &'lean LeanRuntime,
32    project: LakeProject,
33}
34
35impl fmt::Debug for LeanHost<'_> {
36    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
37        f.debug_struct("LeanHost").finish_non_exhaustive()
38    }
39}
40
41impl<'lean> LeanHost<'lean> {
42    /// Bind a host to the runtime and a Lake project root directory.
43    ///
44    /// # Errors
45    ///
46    /// Returns [`lean_rs::LeanError::Host`] with stage
47    /// [`lean_rs::HostStage::Load`] if `path` does not exist or is not a
48    /// directory.
49    pub fn from_lake_project(runtime: &'lean LeanRuntime, path: impl AsRef<Path>) -> LeanResult<Self> {
50        let project = LakeProject::new(path)?;
51        Ok(Self { runtime, project })
52    }
53
54    /// Load the compiled capability dylib for the named
55    /// `(package, lib_name)` pair, initialize its root module, and
56    /// pre-resolve the session symbol addresses.
57    ///
58    /// `package` is the Lake package name (e.g. `"lean_rs_fixture"`);
59    /// `lib_name` is the Lake `lean_lib` declaration name and, by
60    /// convention, also the root Lean module path
61    /// (e.g. `"LeanRsFixture"`). For projects where these differ the
62    /// `lib_name` argument is also the module that gets initialised.
63    ///
64    /// # Errors
65    ///
66    /// Returns [`lean_rs::LeanError::Host`] with stage
67    /// [`lean_rs::HostStage::Load`] if the dylib does not exist or fails
68    /// to open, [`lean_rs::HostStage::Link`] if the initializer symbol or
69    /// any of the twenty-six mandatory session symbols is missing. The
70    /// four optional `MetaM` symbols (`infer_type`, `whnf`,
71    /// `heartbeat_burn`, `is_def_eq`) are looked up lazily and their
72    /// absence does not fail loading; `run_meta` reports `Unsupported`
73    /// at call time.
74    pub fn load_capabilities<'h>(&'h self, package: &str, lib_name: &str) -> LeanResult<LeanCapabilities<'lean, 'h>> {
75        let dylib_path = self.project.capability_dylib(package, lib_name);
76        let library = LeanLibrary::open(self.runtime, &dylib_path)?;
77        LeanCapabilities::new(self, library, package, lib_name)
78    }
79
80    /// The runtime borrow this host was constructed with.
81    pub(crate) fn runtime(&self) -> &'lean LeanRuntime {
82        self.runtime
83    }
84
85    /// The Lake project root, for capability code that needs to pass
86    /// the path through to Lean (e.g., setting `Lean.searchPathRef`).
87    pub(crate) fn project(&self) -> &LakeProject {
88        &self.project
89    }
90}
lean_rs_host/host/host.rs

lean_rs_host/host/
host.rs
