lean_toolchain/
loader.rs

1//! Loader-side data types shared between `lean-rs` (runtime opener) and the
2//! worker wire protocol (parent ↔ child serialisation).
3//!
4//! These types live in `lean-toolchain` because the worker-protocol crate needs
5//! them on the wire and must not depend on `lean-rs` (which would re-link
6//! `libleanshared` into every parent process). `lean-rs` re-exports them at
7//! their historical paths (`lean_rs::module::*`) for source compatibility.
8
9use std::path::{Path, PathBuf};
10
11/// Stable preflight diagnostic codes for manifest-backed capability loading.
12///
13/// Single source of truth shared between the runtime preflight in `lean-rs`
14/// and the wire payloads in the worker-protocol crate.
15#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
16pub enum LeanLoaderDiagnosticCode {
17    /// The manifest path was absent, unreadable, or pointed at a missing file.
18    MissingManifest,
19    /// The manifest was not valid JSON or missed required fields.
20    MalformedManifest,
21    /// The manifest schema version is newer or otherwise unsupported.
22    UnsupportedManifestSchema,
23    /// The manifest's primary capability dylib is missing.
24    MissingPrimaryDylib,
25    /// A dependency dylib named by the manifest is missing.
26    MissingTransitiveDependency,
27    /// A dylib could not be parsed as a native object for this platform.
28    UnsupportedArchitecture,
29    /// The manifest was produced by an unsupported or mismatched Lean toolchain.
30    UnsupportedToolchainFingerprint,
31    /// A manifest appears older than the build artifact it describes.
32    StaleManifest,
33    /// The root module initializer named by the manifest is not exported.
34    MissingInitializer,
35    /// A Lean/imported symbol is not supplied by the manifest dependency set.
36    MissingImportedSymbol,
37}
38
39impl LeanLoaderDiagnosticCode {
40    /// Stable string identifier suitable for logs and support reports.
41    #[must_use]
42    pub const fn as_str(self) -> &'static str {
43        match self {
44            Self::MissingManifest => "lean_rs.loader.missing_manifest",
45            Self::MalformedManifest => "lean_rs.loader.malformed_manifest",
46            Self::UnsupportedManifestSchema => "lean_rs.loader.unsupported_manifest_schema",
47            Self::MissingPrimaryDylib => "lean_rs.loader.missing_primary_dylib",
48            Self::MissingTransitiveDependency => "lean_rs.loader.missing_transitive_dependency",
49            Self::UnsupportedArchitecture => "lean_rs.loader.unsupported_architecture",
50            Self::UnsupportedToolchainFingerprint => "lean_rs.loader.unsupported_toolchain_fingerprint",
51            Self::StaleManifest => "lean_rs.loader.stale_manifest",
52            Self::MissingInitializer => "lean_rs.loader.missing_initializer",
53            Self::MissingImportedSymbol => "lean_rs.loader.missing_imported_symbol",
54        }
55    }
56}
57
58impl std::fmt::Display for LeanLoaderDiagnosticCode {
59    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
60        f.write_str(self.as_str())
61    }
62}
63
64/// Severity of one loader preflight finding.
65#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
66pub enum LeanLoaderSeverity {
67    /// Informational finding that does not block loading.
68    Info,
69    /// Suspicious state that may still load.
70    Warning,
71    /// The capability should not be opened until this is fixed.
72    Error,
73}
74
75/// Maximum bytes preserved in user-facing loader diagnostic strings.
76///
77/// Matches the workspace error-message bound so diagnostics that flow back
78/// through `LeanError` are not double-truncated.
79pub const LOADER_DIAGNOSTIC_TEXT_LIMIT: usize = 4 * 1024;
80
81/// Truncate `text` to at most [`LOADER_DIAGNOSTIC_TEXT_LIMIT`] bytes on a
82/// UTF-8 char boundary.
83#[must_use]
84pub fn bound_loader_text(mut text: String) -> String {
85    if text.len() <= LOADER_DIAGNOSTIC_TEXT_LIMIT {
86        return text;
87    }
88    let mut cut = LOADER_DIAGNOSTIC_TEXT_LIMIT;
89    while cut > 0 && !text.is_char_boundary(cut) {
90        cut = cut.saturating_sub(1);
91    }
92    text.truncate(cut);
93    text
94}
95
96/// One bounded preflight finding.
97#[derive(Clone, Debug, Eq, PartialEq)]
98pub struct LeanLoaderCheck {
99    code: LeanLoaderDiagnosticCode,
100    severity: LeanLoaderSeverity,
101    subject: String,
102    message: String,
103    repair_hint: String,
104}
105
106impl LeanLoaderCheck {
107    /// Construct an `Error` finding with bounded text fields.
108    #[must_use]
109    pub fn error(
110        code: LeanLoaderDiagnosticCode,
111        subject: impl Into<String>,
112        message: impl Into<String>,
113        repair_hint: impl Into<String>,
114    ) -> Self {
115        Self {
116            code,
117            severity: LeanLoaderSeverity::Error,
118            subject: bound_loader_text(subject.into()),
119            message: bound_loader_text(message.into()),
120            repair_hint: bound_loader_text(repair_hint.into()),
121        }
122    }
123
124    /// Stable loader diagnostic code.
125    #[must_use]
126    pub fn code(&self) -> LeanLoaderDiagnosticCode {
127        self.code
128    }
129
130    /// Whether this finding blocks capability loading.
131    #[must_use]
132    pub fn severity(&self) -> LeanLoaderSeverity {
133        self.severity
134    }
135
136    /// Artifact, symbol, or manifest field this finding is about.
137    #[must_use]
138    pub fn subject(&self) -> &str {
139        &self.subject
140    }
141
142    /// Bounded explanation of the failure.
143    #[must_use]
144    pub fn message(&self) -> &str {
145        &self.message
146    }
147
148    /// Bounded repair hint for normal users.
149    #[must_use]
150    pub fn repair_hint(&self) -> &str {
151        &self.repair_hint
152    }
153}
154
155impl std::fmt::Display for LeanLoaderCheck {
156    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
157        write!(
158            f,
159            "{} [{:?}] {}: {} (repair: {})",
160            self.code.as_str(),
161            self.severity,
162            self.subject,
163            self.message,
164            self.repair_hint
165        )
166    }
167}
168
169/// Structured result of loader preflight for one capability manifest.
170#[derive(Clone, Debug, Eq, PartialEq)]
171pub struct LeanLoaderReport {
172    manifest_path: Option<PathBuf>,
173    checks: Vec<LeanLoaderCheck>,
174}
175
176impl LeanLoaderReport {
177    /// Bundle preflight findings with the manifest path they concern.
178    #[must_use]
179    pub fn new(manifest_path: Option<PathBuf>, checks: Vec<LeanLoaderCheck>) -> Self {
180        Self { manifest_path, checks }
181    }
182
183    /// Manifest path checked, if the descriptor resolved one.
184    #[must_use]
185    pub fn manifest_path(&self) -> Option<&Path> {
186        self.manifest_path.as_deref()
187    }
188
189    /// All preflight findings.
190    #[must_use]
191    pub fn checks(&self) -> &[LeanLoaderCheck] {
192        &self.checks
193    }
194
195    /// Blocking findings only.
196    pub fn errors(&self) -> impl Iterator<Item = &LeanLoaderCheck> {
197        self.checks
198            .iter()
199            .filter(|check| check.severity == LeanLoaderSeverity::Error)
200    }
201
202    /// Whether preflight found no blocking findings.
203    #[must_use]
204    pub fn is_ok(&self) -> bool {
205        self.errors().next().is_none()
206    }
207
208    /// First blocking finding, if any.
209    #[must_use]
210    pub fn first_error(&self) -> Option<&LeanLoaderCheck> {
211        self.errors().next()
212    }
213
214    /// Consume the report and return its findings.
215    #[must_use]
216    pub fn into_checks(self) -> Vec<LeanLoaderCheck> {
217        self.checks
218    }
219}
220
221/// Initializer for a Lean module hosted by a loaded dylib.
222#[derive(Clone, Debug, Eq, PartialEq)]
223pub struct LeanModuleInitializer {
224    package: String,
225    module: String,
226}
227
228impl LeanModuleInitializer {
229    /// Create an initializer descriptor from Lake package and root module names.
230    #[must_use]
231    pub fn new(package: impl Into<String>, module: impl Into<String>) -> Self {
232        Self {
233            package: package.into(),
234            module: module.into(),
235        }
236    }
237
238    /// Lake package name used by the initializer.
239    #[must_use]
240    pub fn package_name(&self) -> &str {
241        &self.package
242    }
243
244    /// Root Lean module name used by the initializer.
245    #[must_use]
246    pub fn module_name(&self) -> &str {
247        &self.module
248    }
249}
250
251/// Dependency dylib that must stay alive while a capability is loaded.
252#[derive(Clone, Debug, Eq, PartialEq)]
253pub struct LeanLibraryDependency {
254    path: PathBuf,
255    exports_symbols_for_dependents: bool,
256    initializer: Option<LeanModuleInitializer>,
257}
258
259impl LeanLibraryDependency {
260    /// Add a dependency dylib to the bundle.
261    #[must_use]
262    pub fn path(path: impl Into<PathBuf>) -> Self {
263        Self {
264            path: path.into(),
265            exports_symbols_for_dependents: false,
266            initializer: None,
267        }
268    }
269
270    /// Make this dependency's Lean symbols available to later dylibs in the
271    /// same bundle.
272    ///
273    /// This is a capability-level requirement, not a platform-loader flag in
274    /// the public contract. On ELF platforms it maps to global symbol
275    /// visibility; other platforms use the equivalent behavior provided by the
276    /// native loader.
277    #[must_use]
278    pub fn export_symbols_for_dependents(mut self) -> Self {
279        self.exports_symbols_for_dependents = true;
280        self
281    }
282
283    /// Initialize a module from this dependency after it is opened.
284    #[must_use]
285    pub fn initializer(mut self, package: impl Into<String>, module: impl Into<String>) -> Self {
286        self.initializer = Some(LeanModuleInitializer::new(package, module));
287        self
288    }
289
290    /// On-disk path to the dependency dylib.
291    #[must_use]
292    pub fn path_ref(&self) -> &Path {
293        &self.path
294    }
295
296    /// Whether symbols from this dependency are exported to later bundle
297    /// members.
298    #[must_use]
299    pub fn exports_symbols_for_dependents(&self) -> bool {
300        self.exports_symbols_for_dependents
301    }
302
303    /// Optional module initializer for this dependency.
304    #[must_use]
305    pub fn module_initializer(&self) -> Option<&LeanModuleInitializer> {
306        self.initializer.as_ref()
307    }
308
309    /// Consume the dependency and return its module initializer, if any.
310    ///
311    /// Used by the runtime opener (`lean-rs`) to take owned ownership of the
312    /// initializer when opening the bundle, without re-cloning the strings.
313    #[must_use]
314    pub fn into_module_initializer(self) -> Option<LeanModuleInitializer> {
315        self.initializer
316    }
317}
lean_toolchain/loader.rs

lean_toolchain/
loader.rs
