1use std::path::{Path, PathBuf};
9
10use super::preflight::{CapabilityManifest, LeanCapabilityPreflight, manifest_error_to_lean_error};
11use super::{LeanLibrary, LeanLibraryBundle, LeanLibraryDependency, LeanModule};
12use crate::error::{LeanError, LeanResult};
13use crate::runtime::LeanRuntime;
14
15#[derive(Clone, Debug, Eq, PartialEq)]
17pub struct LeanBuiltCapability {
18 dylib_path: Option<PathBuf>,
19 env_var: Option<String>,
20 manifest_path: Option<PathBuf>,
21 manifest_env_var: Option<String>,
22 package: Option<String>,
23 module: Option<String>,
24 dependencies: Vec<LeanLibraryDependency>,
25}
26
27impl LeanBuiltCapability {
28 #[must_use]
40 pub fn path(path: impl Into<PathBuf>) -> Self {
41 Self {
42 dylib_path: Some(path.into()),
43 env_var: None,
44 manifest_path: None,
45 manifest_env_var: None,
46 package: None,
47 module: None,
48 dependencies: Vec::new(),
49 }
50 }
51
52 #[must_use]
59 pub fn env(env_var: impl Into<String>) -> Self {
60 Self {
61 dylib_path: None,
62 env_var: Some(env_var.into()),
63 manifest_path: None,
64 manifest_env_var: None,
65 package: None,
66 module: None,
67 dependencies: Vec::new(),
68 }
69 }
70
71 #[must_use]
82 pub fn manifest_path(path: impl Into<PathBuf>) -> Self {
83 Self {
84 dylib_path: None,
85 env_var: None,
86 manifest_path: Some(path.into()),
87 manifest_env_var: None,
88 package: None,
89 module: None,
90 dependencies: Vec::new(),
91 }
92 }
93
94 #[must_use]
101 pub fn manifest_env(env_var: impl Into<String>) -> Self {
102 Self {
103 dylib_path: None,
104 env_var: None,
105 manifest_path: None,
106 manifest_env_var: Some(env_var.into()),
107 package: None,
108 module: None,
109 dependencies: Vec::new(),
110 }
111 }
112
113 #[must_use]
115 pub fn env_var(mut self, env_var: impl Into<String>) -> Self {
116 self.env_var = Some(env_var.into());
117 self
118 }
119
120 #[must_use]
122 pub fn manifest_env_var(mut self, env_var: impl Into<String>) -> Self {
123 self.manifest_env_var = Some(env_var.into());
124 self
125 }
126
127 #[must_use]
129 pub fn package(mut self, package: impl Into<String>) -> Self {
130 self.package = Some(package.into());
131 self
132 }
133
134 #[must_use]
136 pub fn module(mut self, module: impl Into<String>) -> Self {
137 self.module = Some(module.into());
138 self
139 }
140
141 #[must_use]
147 pub fn dependency(mut self, dependency: LeanLibraryDependency) -> Self {
148 self.dependencies.push(dependency);
149 self
150 }
151
152 #[must_use]
155 pub fn dependencies(mut self, dependencies: impl IntoIterator<Item = LeanLibraryDependency>) -> Self {
156 self.dependencies.extend(dependencies);
157 self
158 }
159
160 #[must_use]
162 pub fn package_name(&self) -> Option<&str> {
163 self.package.as_deref()
164 }
165
166 #[must_use]
168 pub fn module_name(&self) -> Option<&str> {
169 self.module.as_deref()
170 }
171
172 #[must_use]
174 pub fn dependency_descriptors(&self) -> &[LeanLibraryDependency] {
175 &self.dependencies
176 }
177
178 pub fn dylib_path(&self) -> LeanResult<PathBuf> {
185 if let Some(path) = &self.dylib_path {
186 return Ok(path.clone());
187 }
188 let env_var = self.env_var.as_deref().ok_or_else(|| {
189 LeanError::module_init("LeanBuiltCapability needs either a dylib path or an environment variable")
190 })?;
191 std::env::var_os(env_var).map(PathBuf::from).ok_or_else(|| {
192 LeanError::module_init(format!(
193 "environment variable {env_var} is not set for Lean capability dylib"
194 ))
195 })
196 }
197
198 pub fn resolved_manifest_path(&self) -> LeanResult<PathBuf> {
205 if let Some(path) = &self.manifest_path {
206 return Ok(path.clone());
207 }
208 let env_var = self.manifest_env_var.as_deref().ok_or_else(|| {
209 LeanError::module_init("LeanBuiltCapability needs either a manifest path or manifest environment variable")
210 })?;
211 std::env::var_os(env_var).map(PathBuf::from).ok_or_else(|| {
212 LeanError::module_init(format!(
213 "environment variable {env_var} is not set for Lean capability manifest"
214 ))
215 })
216 }
217}
218
219impl From<&lean_toolchain::BuiltLeanCapability> for LeanBuiltCapability {
220 fn from(value: &lean_toolchain::BuiltLeanCapability) -> Self {
221 Self {
222 dylib_path: Some(value.dylib_path().to_path_buf()),
223 env_var: Some(value.env_var().to_owned()),
224 manifest_path: Some(value.manifest_path().to_path_buf()),
225 manifest_env_var: Some(value.manifest_env_var().to_owned()),
226 package: Some(value.package().to_owned()),
227 module: Some(value.module().to_owned()),
228 dependencies: Vec::new(),
229 }
230 }
231}
232
233pub struct LeanCapability<'lean> {
236 bundle: LeanLibraryBundle<'lean>,
237 package: String,
238 module: String,
239}
240
241impl<'lean> LeanCapability<'lean> {
242 #[allow(clippy::needless_pass_by_value)]
251 pub fn from_build_manifest(runtime: &'lean LeanRuntime, spec: LeanBuiltCapability) -> LeanResult<Self> {
252 let report = LeanCapabilityPreflight::new(spec.clone()).check();
253 if !report.is_ok() {
254 return Err(report.into_error());
255 }
256 let manifest_path = spec.resolved_manifest_path()?;
257 let manifest = CapabilityManifest::read(&manifest_path).map_err(manifest_error_to_lean_error)?;
258 Self::open_with_dependencies(
259 runtime,
260 manifest.primary_dylib,
261 manifest.package,
262 manifest.module,
263 manifest.dependencies,
264 )
265 }
266
267 pub fn from_build_env(runtime: &'lean LeanRuntime, mut spec: LeanBuiltCapability) -> LeanResult<Self> {
279 let dylib_path = spec.dylib_path()?;
280 let package = spec.package.take().ok_or_else(|| {
281 LeanError::linking("LeanBuiltCapability is missing the Lake package name; call `.package(...)`")
282 })?;
283 let module = spec.module.take().ok_or_else(|| {
284 LeanError::linking("LeanBuiltCapability is missing the root Lean module name; call `.module(...)`")
285 })?;
286 Self::open_with_dependencies(runtime, dylib_path, package, module, spec.dependencies)
287 }
288
289 pub fn open(
297 runtime: &'lean LeanRuntime,
298 dylib_path: impl AsRef<Path>,
299 package: impl Into<String>,
300 module: impl Into<String>,
301 ) -> LeanResult<Self> {
302 let package = package.into();
303 let module = module.into();
304 Self::open_with_dependencies(runtime, dylib_path, package, module, [])
305 }
306
307 pub fn open_with_dependencies(
319 runtime: &'lean LeanRuntime,
320 dylib_path: impl AsRef<Path>,
321 package: impl Into<String>,
322 module: impl Into<String>,
323 dependencies: impl IntoIterator<Item = LeanLibraryDependency>,
324 ) -> LeanResult<Self> {
325 let package = package.into();
326 let module = module.into();
327 let bundle = LeanLibraryBundle::open(runtime, dylib_path, dependencies)?;
328 let _module = bundle.initialize_module(&package, &module)?;
329 Ok(Self {
330 bundle,
331 package,
332 module,
333 })
334 }
335
336 pub fn module(&self) -> LeanResult<LeanModule<'lean, '_>> {
346 self.bundle.initialize_module(&self.package, &self.module)
347 }
348
349 #[must_use]
351 pub fn library(&self) -> &LeanLibrary<'lean> {
352 self.bundle.library()
353 }
354
355 #[must_use]
357 pub fn bundle(&self) -> &LeanLibraryBundle<'lean> {
358 &self.bundle
359 }
360
361 #[must_use]
363 pub fn package_name(&self) -> &str {
364 &self.package
365 }
366
367 #[must_use]
369 pub fn module_name(&self) -> &str {
370 &self.module
371 }
372}
373
374#[cfg(test)]
375#[allow(clippy::expect_used, clippy::panic)]
376mod tests {
377 use super::{CapabilityManifest, LeanBuiltCapability, LeanLibraryDependency};
378 use std::fs;
379 use std::path::PathBuf;
380
381 #[test]
382 fn built_capability_path_is_resolved_without_runtime_env() {
383 let spec = LeanBuiltCapability::path("/tmp/libcap.so")
384 .env_var("LEAN_RS_CAPABILITY_CAP_DYLIB")
385 .package("pkg")
386 .module("Cap");
387
388 let path = match spec.dylib_path() {
389 Ok(path) => path,
390 Err(err) => panic!("expected path, got {err}"),
391 };
392 assert_eq!(path, std::path::PathBuf::from("/tmp/libcap.so"));
393 assert_eq!(spec.package_name(), Some("pkg"));
394 assert_eq!(spec.module_name(), Some("Cap"));
395 }
396
397 #[test]
398 fn missing_runtime_env_is_typed() {
399 let spec = LeanBuiltCapability::env("LEAN_RS_TEST_MISSING_CAPABILITY_DYLIB")
400 .package("pkg")
401 .module("Cap");
402 let err = match spec.dylib_path() {
403 Ok(path) => panic!("expected missing env error, got {}", path.display()),
404 Err(err) => err,
405 };
406 assert_eq!(err.code(), crate::LeanDiagnosticCode::ModuleInit);
407 }
408
409 #[test]
410 fn missing_runtime_manifest_env_is_typed() {
411 let spec = LeanBuiltCapability::manifest_env("LEAN_RS_TEST_MISSING_CAPABILITY_MANIFEST");
412 let err = match spec.resolved_manifest_path() {
413 Ok(path) => panic!("expected missing manifest env error, got {}", path.display()),
414 Err(err) => err,
415 };
416 assert_eq!(err.code(), crate::LeanDiagnosticCode::ModuleInit);
417 }
418
419 #[test]
420 fn manifest_descriptor_parses_dependencies() {
421 let path = temp_manifest_path("manifest_descriptor_parses_dependencies");
422 write_manifest(
423 &path,
424 r#"{
425 "schema_version": 1,
426 "target_name": "Cap",
427 "package": "pkg",
428 "module": "Cap",
429 "primary_dylib": "/tmp/libcap.so",
430 "dependencies": [
431 {
432 "dylib_path": "/tmp/libdep.so",
433 "export_symbols_for_dependents": true,
434 "initializer": { "package": "dep_pkg", "module": "Dep" }
435 }
436 ]
437}"#,
438 );
439
440 let manifest = match CapabilityManifest::read(&path) {
441 Ok(manifest) => manifest,
442 Err(err) => panic!("expected manifest to parse, got {err}"),
443 };
444 assert_eq!(manifest.primary_dylib, PathBuf::from("/tmp/libcap.so"));
445 assert_eq!(manifest.package, "pkg");
446 assert_eq!(manifest.module, "Cap");
447 assert_eq!(manifest.dependencies.len(), 1);
448 let Some(dependency) = manifest.dependencies.first() else {
449 panic!("expected one dependency");
450 };
451 assert!(dependency.exports_symbols_for_dependents());
452 assert_eq!(dependency.path_ref(), std::path::Path::new("/tmp/libdep.so"));
453 let Some(initializer) = dependency.module_initializer() else {
454 panic!("expected dependency initializer");
455 };
456 assert_eq!(initializer.package_name(), "dep_pkg");
457 assert_eq!(initializer.module_name(), "Dep");
458 }
459
460 #[test]
461 fn unsupported_manifest_schema_is_typed() {
462 let path = temp_manifest_path("unsupported_manifest_schema_is_typed");
463 write_manifest(
464 &path,
465 r#"{
466 "schema_version": 999,
467 "package": "pkg",
468 "module": "Cap",
469 "primary_dylib": "/tmp/libcap.so"
470}"#,
471 );
472
473 let Err(err) = CapabilityManifest::read(&path) else {
474 panic!("expected unsupported schema error");
475 };
476 assert_eq!(err.code(), crate::LeanLoaderDiagnosticCode::UnsupportedManifestSchema);
477 assert!(err.message().contains("unsupported Lean capability manifest schema"));
478 }
479
480 #[test]
481 fn built_capability_records_dependency_descriptors() {
482 let spec = LeanBuiltCapability::path("/tmp/libcap.so").dependency(
483 LeanLibraryDependency::path("/tmp/libdep.so")
484 .export_symbols_for_dependents()
485 .initializer("dep_pkg", "Dep"),
486 );
487
488 let dependencies = spec.dependency_descriptors();
489 assert_eq!(dependencies.len(), 1);
490 let Some(dependency) = dependencies.first() else {
491 panic!("expected one dependency descriptor");
492 };
493 assert!(dependency.exports_symbols_for_dependents());
494 let Some(initializer) = dependency.module_initializer() else {
495 panic!("dependency initializer is recorded");
496 };
497 assert_eq!(initializer.package_name(), "dep_pkg");
498 assert_eq!(initializer.module_name(), "Dep");
499 }
500
501 fn temp_manifest_path(name: &str) -> PathBuf {
502 let dir = std::env::temp_dir().join(format!("lean-rs-manifest-{}-{name}", std::process::id()));
503 drop(fs::remove_dir_all(&dir));
504 fs::create_dir_all(&dir).expect("create manifest test dir");
505 dir.join("capability.json")
506 }
507
508 fn write_manifest(path: &std::path::Path, contents: &str) {
509 fs::write(path, contents).expect("write manifest fixture");
510 }
511}