lean_toolchain/
lib.rs

1//! Lean 4 toolchain discovery, fingerprinting, allowlist re-export, and build-script helpers.
2//!
3//! Sits one layer above [`lean_rs_abi`], which owns link-free ABI/toolchain metadata. This crate
4//! composes on top: a typed [`ToolchainFingerprint`], the workspace-only Lake [`LAKE_FIXTURE_DIGEST`], a layered
5//! [`LinkDiagnostics`] error type, and reusable build-script helpers
6//! ([`emit_lean_link_directives_checked`], [`build_lake_target`],
7//! [`build_lake_target_quiet`]) that downstream embedders and higher layers can use to get
8//! consistent link/rerun directives and Lake dylib paths without duplicating policy.
9//!
10//! ## Single typed entry point
11//!
12//! [`LEAN_VERSION`], [`LEAN_HEADER_PATH`], [`LEAN_HEADER_DIGEST`], and [`LEAN_RESOLVED_VERSION`]
13//! are resolved by this crate's `build.rs` (probing the active toolchain, degrading to the latest
14//! supported entry when none is installed), so embedders need only one import for build metadata.
15//! Live toolchain identity lives here, not in [`lean_rs_abi`], which is purely static. The
16//! allowlist comes through [`required_symbols`] (no copy).
17//!
18//! ## Layering
19//!
20//! `lean-rs-abi → lean-toolchain` for link-free metadata, and `lean-rs-sys → lean-rs`
21//! for raw runtime FFI. Raw `lean_*` symbols never appear in this crate's public surface.
22
23#![forbid(unsafe_code)]
24
25mod build_helpers;
26mod built_capability;
27mod diagnostics;
28mod discover;
29mod fingerprint;
30mod lakefile_toml;
31mod limits;
32mod loader;
33pub mod manifest_validation;
34mod modules;
35mod source_package;
36
37pub use build_helpers::{
38    BuiltLeanCapability, CAPABILITY_MANIFEST_SCHEMA_VERSION, CargoLeanCapability, build_lake_target,
39    build_lake_target_quiet, capability_env_var, capability_manifest_env_var, emit_lean_link_directives,
40    emit_lean_link_directives_checked,
41};
42pub use built_capability::{BuiltCapabilityArtifact, LeanBuiltCapability, LeanBuiltCapabilityError};
43pub use diagnostics::LinkDiagnostics;
44pub use discover::{DiscoverOptions, DiscoverySource, ToolchainInfo, discover_toolchain};
45pub use fingerprint::{
46    HOST_TRIPLE, LAKE_FIXTURE_DIGEST, LEAN_HEADER_DIGEST, LEAN_HEADER_PATH, LEAN_RESOLVED_VERSION, LEAN_VERSION,
47    ToolchainFingerprint,
48};
49pub use lean_rs_abi::{SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_by_digest, supported_for};
50pub use limits::{
51    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX, LEAN_HEARTBEAT_LIMIT_DEFAULT,
52    LEAN_HEARTBEAT_LIMIT_MAX,
53};
54pub use loader::{
55    LOADER_DIAGNOSTIC_TEXT_LIMIT, LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership, LeanExportResultConvention,
56    LeanExportReturnAbi, LeanExportSignature, LeanExportSymbolKind, LeanLibraryDependency, LeanLoaderCheck,
57    LeanLoaderDiagnosticCode, LeanLoaderReport, LeanLoaderSeverity, LeanModuleInitializer, bound_loader_text,
58};
59pub use manifest_validation::CapabilityManifest;
60pub use modules::{
61    LeanLakeProjectModules, LeanModuleDescriptor, LeanModuleDiscoveryDiagnostic, LeanModuleDiscoveryOptions,
62    LeanModuleSetFingerprint, discover_lake_modules,
63};
64pub use source_package::{
65    GeneratedSourceFile, MaterializedSourcePackage, SourcePackageError, SourcePackageManifestPolicy,
66    SourcePackageMaterializationRequest, SourcePackageProvenance, materialize_source_package,
67};
68
69/// Version of the `lean-toolchain` crate, matching `Cargo.toml`.
70pub const VERSION: &str = env!("CARGO_PKG_VERSION");
71
72/// Curated allowlist of `LEAN_EXPORT` symbols the workspace relies on.
73///
74/// Returns [`lean_rs_abi::REQUIRED_SYMBOLS`] directly—the allowlist lives in
75/// exactly one place. Use this through `lean-toolchain` so consumer crates do
76/// not also need a direct raw-FFI dependency just to enumerate symbol
77/// names.
78#[must_use]
79pub fn required_symbols() -> &'static [&'static str] {
80    lean_rs_abi::REQUIRED_SYMBOLS
81}
82
83#[cfg(test)]
84mod tests {
85    use super::{LEAN_HEADER_DIGEST, LEAN_VERSION, VERSION, required_symbols};
86
87    #[test]
88    fn version_constant_matches_package() {
89        assert_eq!(VERSION, env!("CARGO_PKG_VERSION"));
90    }
91
92    #[test]
93    fn required_symbols_is_nonempty() {
94        assert!(!required_symbols().is_empty());
95    }
96
97    #[test]
98    fn lean_metadata_is_baked() {
99        assert!(!LEAN_VERSION.is_empty());
100        assert_eq!(LEAN_HEADER_DIGEST.len(), 64);
101        assert!(LEAN_HEADER_DIGEST.chars().all(|c| c.is_ascii_hexdigit()));
102    }
103}
lean_toolchain/lib.rs

lean_toolchain/
lib.rs
