lean_rs_host/host/

capabilities.rs

//! `LeanCapabilities` — loaded user, generic interop, and host shim
//! dylibs with session symbol addresses pre-resolved.
//!
//! [`LeanCapabilities`] owns three [`lean_rs::module::LeanLibrary`]
//! handles and caches the session symbol addresses that
//! [`crate::host::LeanSession`] dispatches through:
//!
//! - The **user's capability dylib** is the artefact the consumer
//!   built with `lake build` and named in
//!   [`crate::host::LeanHost::load_capabilities`]. It contains the
//!   user's own `@[export]` symbols ([`crate::LeanSession::call_capability`]
//!   dispatches here).
//! - The **generic interop dylib** is
//!   `liblean__rs__interop__shims_LeanRsInterop.dylib`; it carries
//!   reusable callback helpers imported by the host progress shims.
//! - The **shim dylib** is `liblean__rs__host__shims_LeanRsHostShims.dylib`,
//!   built from the `lean-rs-host` crate's bundled shim sources. It contains
//!   the 28 mandatory + 6 optional `lean_rs_host_*` `@[export]` symbols that
//!   every typed `LeanSession` method dispatches through. Lake does *not*
//!   transitively bundle the shim's `@[export]` symbols into the user's dylib
//!   (verified at carve-out time, 2026-05-18 — `LeanLib.sharedFacet` is a
//!   per-package shared library, not a transitive merge), so the host stack
//!   loads the generic interop dylib, host shim dylib, and user dylib
//!   explicitly. All dylibs share one Lean runtime; each per-module
//!   `initialize_<Module>` short-circuits idempotently on its own flag.
//!
//! A missing mandatory shim symbol fails capability load; a missing
//! meta-service symbol degrades to a synthesised
//! [`crate::host::meta::LeanMetaResponse::Unsupported`] at the
//! [`crate::LeanSession::run_meta`] call site. Pre-resolution at
//! construction means each later query is one struct-field read and
//! one FFI call — no per-query `dlsym`.
//!
//! Construction goes through [`crate::host::LeanHost::load_capabilities`];
//! [`LeanCapabilities::session`] then imports a module list and returns
//! the long-lived [`crate::host::LeanSession`] handle.

use core::fmt;

use crate::host::cancellation::LeanCancellationToken;
use crate::host::host::LeanHost;
use crate::host::progress::LeanProgressSink;
use crate::host::session::{LeanSession, SessionSymbols};
use lean_rs::error::LeanResult;
use lean_rs::module::LeanLibrary;

/// Loaded capability, generic interop, and host shim dylibs with session
/// symbol addresses pre-resolved.
///
/// Owns the [`LeanLibrary`] handles so callers do not have to track
/// the dylibs' lifetimes separately. Borrows from the parent
/// [`LeanHost`] for the runtime + project context. Neither [`Send`] nor
/// [`Sync`]: inherited from the contained `LeanLibrary` handles.
pub struct LeanCapabilities<'lean, 'h> {
    host: &'h LeanHost<'lean>,
    /// User's capability dylib — the one named in `load_capabilities`.
    /// `pub(crate)` accessor below exposes it to
    /// [`crate::LeanSession::call_capability`] for ad-hoc dispatch on
    /// user-authored `@[export]` symbols.
    user_library: LeanLibrary<'lean>,
    /// Generic interop shim dylib carrying reusable callback helpers used by
    /// host progress shims. Loaded globally before the host shim dylib so
    /// generated `LeanRsInterop.*` initializer references resolve.
    #[allow(dead_code, reason = "Drop releases the dylib; field is structurally required")]
    interop_library: LeanLibrary<'lean>,
    /// Shim dylib carrying the 28+6 `lean_rs_host_*` `@[export]`
    /// symbols. RAII anchor only — the addresses inside `symbols`
    /// outlive any direct read of this field.
    #[allow(dead_code, reason = "Drop releases the dylib; field is structurally required")]
    shim_library: LeanLibrary<'lean>,
    symbols: SessionSymbols,
}

impl fmt::Debug for LeanCapabilities<'_, '_> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        f.debug_struct("LeanCapabilities").finish_non_exhaustive()
    }
}

impl<'lean, 'h> LeanCapabilities<'lean, 'h> {
    /// Build a [`LeanCapabilities`] from an opened user-capability
    /// library, opening the generic interop and host shim dylibs alongside it.
    ///
    /// Initializes the root module of the user's dylib (idempotent
    /// through Lean's `_G_initialized` short-circuit), opens and
    /// initializes the generic interop and host shim dylibs built from the
    /// crate-owned shim sources, and resolves the
    /// session-dispatch symbol addresses from the **shim** dylib: 28
    /// mandatory baseline symbols (load failure on miss) and 6
    /// optional symbols — five bounded `MetaM` services plus the
    /// info-tree projection (missing entries stored as `None`). Both
    /// [`lean_rs::module::LeanModule`] handles are
    /// dropped at the end of this call — the cached symbol addresses
    /// outlive any single module borrow.
    ///
    /// # Errors
    ///
    /// Returns [`lean_rs::LeanError::Host`] with stage
    /// [`lean_rs::HostStage::Load`] /
    /// [`lean_rs::LeanDiagnosticCode::ModuleInit`] if the bundled shim dylibs
    /// cannot be built or located. Returns [`lean_rs::HostStage::Link`] if the
    /// initializer or any of the 28 **mandatory** symbols is missing from the
    /// shim dylib. Missing optional meta-service symbols never fail capability
    /// load.
    pub(crate) fn new(
        host: &'h LeanHost<'lean>,
        user_library: LeanLibrary<'lean>,
        package: &str,
        lib_name: &str,
    ) -> LeanResult<Self> {
        // Load order matters. The host shim imports LeanRsInterop.Callback,
        // so the generic interop dylib must be global before the host shim
        // initializer runs. Consumers no longer require host shims in their
        // Lake package; the host stack opens and initializes both bundled shim
        // dylibs explicitly before the user dylib initializes.
        let interop_dylib_path = crate::host::lake::LakeProject::interop_dylib()?;
        let interop_library = LeanLibrary::open_globally(host.runtime(), &interop_dylib_path)?;
        let _interop_module = interop_library.initialize_module(
            crate::host::lake::INTEROP_PACKAGE_NAME,
            crate::host::lake::INTEROP_LIB_NAME,
        )?;

        let shim_dylib_path = crate::host::lake::LakeProject::shim_dylib()?;
        let shim_library = LeanLibrary::open_globally(host.runtime(), &shim_dylib_path)?;
        // Explicitly initialize the shim's root module too, so the
        // shim's @[export] functions are live regardless of whether
        // the user's chain reaches them transitively.
        let _shim_module =
            shim_library.initialize_module(crate::host::lake::SHIM_PACKAGE_NAME, crate::host::lake::SHIM_LIB_NAME)?;

        // Now the user dylib. It does not need to depend on the host shims;
        // ad-hoc user exports still resolve from this library.
        let _user_module = user_library.initialize_module(package, lib_name)?;

        // The 28 mandatory + 6 optional `lean_rs_host_*` symbols live
        // in the shim dylib; resolve them there.
        // `LeanSession::call_capability` (separately) routes ad-hoc
        // user-authored `@[export]` symbols through `user_library`.
        let symbols = SessionSymbols::resolve(&shim_library)?;
        Ok(Self {
            host,
            user_library,
            interop_library,
            shim_library,
            symbols,
        })
    }

    /// Import the named modules into a fresh Lean environment and
    /// return a session over the result.
    ///
    /// Imports happen exactly once per `session()` call. The returned
    /// [`LeanSession`] owns the imported environment and reuses this
    /// capability's cached symbol addresses for every query.
    ///
    /// # Errors
    ///
    /// Returns [`lean_rs::LeanError::Cancelled`] if `cancellation` is
    /// already cancelled before import dispatch.
    ///
    /// Returns [`lean_rs::LeanError::LeanException`] if the Lean-side
    /// import raises (missing `.olean`, malformed module name, …),
    /// with the bounded message Lean surfaced.
    pub fn session<'c>(
        &'c self,
        imports: &[&str],
        cancellation: Option<&LeanCancellationToken>,
        progress: Option<&dyn LeanProgressSink>,
    ) -> LeanResult<LeanSession<'lean, 'c>> {
        LeanSession::import(self, imports, cancellation, progress)
    }

    /// The capability's parent host (for runtime + project access by
    /// the session dispatch).
    pub(crate) fn host(&self) -> &'h LeanHost<'lean> {
        self.host
    }

    /// The pre-resolved session symbol addresses.
    pub(crate) fn symbols(&self) -> &SessionSymbols {
        &self.symbols
    }

    /// The user's owned capability [`LeanLibrary`].
    ///
    /// `pub(crate)` so [`crate::LeanSession::call_capability`] can
    /// resolve ad-hoc function symbols on the user's dylib without
    /// holding a separate library borrow. Ad-hoc calls always go to
    /// the user's dylib, not the shim dylib: the shim dylib hosts a
    /// fixed contract (the 28+6 `lean_rs_host_*` symbols pre-resolved
    /// in `symbols`); arbitrary user `@[export]` symbols live in the
    /// user's dylib.
    pub(crate) fn library(&self) -> &LeanLibrary<'lean> {
        &self.user_library
    }
}