pub struct LeanHost<'lean> { /* private fields */ }Expand description
Entry point for hosting Lean capabilities from a Lake project.
Pairs a runtime borrow with a validated Lake project root. Cheap to
construct: only the project root’s existence is checked; no dylib
loading happens until LeanHost::load_capabilities is called.
Neither Send nor Sync: inherited from the contained
&'lean LeanRuntime.
Implementations§
Source§impl<'lean> LeanHost<'lean>
impl<'lean> LeanHost<'lean>
Sourcepub fn from_lake_project(
runtime: &'lean LeanRuntime,
path: impl AsRef<Path>,
) -> LeanResult<Self>
pub fn from_lake_project( runtime: &'lean LeanRuntime, path: impl AsRef<Path>, ) -> LeanResult<Self>
Bind a host to the runtime and a Lake project root directory.
§Errors
Returns lean_rs::LeanError::Host with stage
lean_rs::HostStage::Load if path does not exist or is not a
directory.
Sourcepub fn load_capabilities<'h>(
&'h self,
package: &str,
lib_name: &str,
) -> LeanResult<LeanCapabilities<'lean, 'h>>
pub fn load_capabilities<'h>( &'h self, package: &str, lib_name: &str, ) -> LeanResult<LeanCapabilities<'lean, 'h>>
Load the compiled capability dylib for the named
(package, lib_name) pair, initialize its root module, and
pre-resolve the session symbol addresses.
package is the Lake package name (e.g. "lean_rs_fixture");
lib_name is the Lake lean_lib declaration name and, by
convention, also the root Lean module path
(e.g. "LeanRsFixture"). For projects where these differ the
lib_name argument is also the module that gets initialised.
§Errors
Returns lean_rs::LeanError::Host with stage
lean_rs::HostStage::Load if the dylib does not exist or fails
to open, lean_rs::HostStage::Link if the initializer symbol or
any of the twenty-six mandatory session symbols is missing. The
four optional MetaM symbols (infer_type, whnf,
heartbeat_burn, is_def_eq) are looked up lazily and their
absence does not fail loading; run_meta reports Unsupported
at call time.