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 ad-hoc `@[export]` calls, while
6//! [`LeanHost::load_shims_only`] opens only the bundled host shims for the
7//! standard session services. Both paths pre-resolve the session symbol
8//! addresses and return a [`LeanCapabilities`] that subsequent calls dispatch
9//! through 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 crate::host::capabilities::LeanCapabilities;
18use crate::host::lake::LakeProject;
19use lean_rs::LeanRuntime;
20use lean_rs::error::LeanResult;
21use lean_rs::module::LeanLibrary;
22
23/// Entry point for hosting Lean capabilities from a Lake project.
24///
25/// Pairs a runtime borrow with a validated Lake project root. Cheap to
26/// construct: only the project root's existence is checked; no dylib
27/// loading happens until [`LeanHost::load_capabilities`] is called.
28///
29/// Neither [`Send`] nor [`Sync`]: inherited from the contained
30/// `&'lean LeanRuntime`.
31pub struct LeanHost<'lean> {
32    runtime: &'lean LeanRuntime,
33    project: LakeProject,
34}
35
36impl fmt::Debug for LeanHost<'_> {
37    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
38        f.debug_struct("LeanHost").finish_non_exhaustive()
39    }
40}
41
42impl<'lean> LeanHost<'lean> {
43    /// Bind a host to the runtime and a Lake project root directory.
44    ///
45    /// # Errors
46    ///
47    /// Returns [`lean_rs::LeanError::Host`] with stage
48    /// [`lean_rs::HostStage::Load`] if `path` does not exist or is not a
49    /// directory.
50    pub fn from_lake_project(runtime: &'lean LeanRuntime, path: impl AsRef<Path>) -> LeanResult<Self> {
51        let project = LakeProject::new(path)?;
52        Ok(Self { runtime, project })
53    }
54
55    /// Load the compiled capability dylib for the named
56    /// `(package, lib_name)` pair, initialize its root module, and
57    /// pre-resolve the session symbol addresses.
58    ///
59    /// `package` is the Lake package name (e.g. `"lean_rs_fixture"`);
60    /// `lib_name` is the Lake `lean_lib` declaration name and, by
61    /// convention, also the root Lean module path
62    /// (e.g. `"LeanRsFixture"`). For projects where these differ the
63    /// `lib_name` argument is also the module that gets initialised.
64    ///
65    /// # Errors
66    ///
67    /// Returns [`lean_rs::LeanError::Host`] with stage
68    /// [`lean_rs::HostStage::Load`] if the dylib does not exist or fails
69    /// to open, [`lean_rs::HostStage::Link`] if the initializer symbol or
70    /// any of the twenty-eight mandatory session symbols is missing. The
71    /// four optional `MetaM` symbols (`infer_type`, `whnf`,
72    /// `heartbeat_burn`, `is_def_eq`) are looked up lazily and their
73    /// absence does not fail loading; `run_meta` reports `Unsupported`
74    /// at call time.
75    pub fn load_capabilities<'h>(&'h self, package: &str, lib_name: &str) -> LeanResult<LeanCapabilities<'lean, 'h>> {
76        let dylib_path = self.project.capability_dylib(package, lib_name);
77        let library = LeanLibrary::open(self.runtime, &dylib_path)?;
78        LeanCapabilities::new(self, library, package, lib_name)
79    }
80
81    /// Load the bundled host-shim and interop dylibs without opening a user
82    /// capability dylib.
83    ///
84    /// Sessions opened from the returned capabilities can import modules from
85    /// this Lake project's `.olean` search path and use the standard
86    /// shim-backed Meta, elaboration, kernel, info-tree, declaration, and
87    /// source-range services. [`crate::LeanSession::call_capability`] returns
88    /// [`lean_rs::LeanDiagnosticCode::Unsupported`] because there is no user
89    /// library to dispatch arbitrary `@[export]` symbols through.
90    ///
91    /// # Errors
92    ///
93    /// Returns [`lean_rs::LeanError::Host`] with stage
94    /// [`lean_rs::HostStage::Load`] / [`lean_rs::LeanDiagnosticCode::ModuleInit`]
95    /// if the bundled shim or interop dylibs cannot be built or located.
96    /// Returns [`lean_rs::HostStage::Link`] if any mandatory shim symbol is
97    /// missing.
98    pub fn load_shims_only<'h>(&'h self) -> LeanResult<LeanCapabilities<'lean, 'h>> {
99        LeanCapabilities::new_shims_only(self)
100    }
101
102    /// The runtime borrow this host was constructed with.
103    pub(crate) fn runtime(&self) -> &'lean LeanRuntime {
104        self.runtime
105    }
106
107    /// The Lake project root, for capability code that needs to pass
108    /// the path through to Lean (e.g., setting `Lean.searchPathRef`).
109    pub(crate) fn project(&self) -> &LakeProject {
110        &self.project
111    }
112}
lean_rs_host/host/host.rs

lean_rs_host/host/
host.rs
