lean_toolchain/
lib.rs

1//! Lean 4 toolchain discovery, fingerprinting, allowlist re-export, and build-script helpers.
2//!
3//! Sits one layer above the workspace crate [`lean_rs_sys`], which owns the raw `extern "C"`
4//! declarations, the hand-written refcount inline helpers, the signature-checked symbol
5//! allowlist, the header SHA-256 digest, and the link directives. This crate composes on top:
6//! a typed [`ToolchainFingerprint`], the workspace-only Lake [`LAKE_FIXTURE_DIGEST`], a layered
7//! [`LinkDiagnostics`] error type, and reusable build-script helpers
8//! ([`emit_lean_link_directives_checked`], [`build_lake_target`],
9//! [`build_lake_target_quiet`]) that downstream embedders and higher layers can use to get
10//! consistent link/rerun directives and Lake dylib paths without duplicating policy.
11//!
12//! ## Single typed entry point
13//!
14//! [`LEAN_VERSION`], [`LEAN_HEADER_PATH`], and [`LEAN_HEADER_DIGEST`] are re-exported from
15//! [`lean_rs_sys`] so embedders that depend on this crate need only one import for build
16//! metadata. The allowlist comes through [`required_symbols`] (no copy).
17//!
18//! ## Layering
19//!
20//! `lean-rs-sys → lean-toolchain → lean-rs`. Raw `lean_*` symbols never appear in this
21//! crate's public surface—they remain in `lean-rs-sys` and reach the safe layers through
22//! `lean-rs`'s `pub(crate)` modules.
23
24#![forbid(unsafe_code)]
25
26mod build_helpers;
27mod built_capability;
28mod diagnostics;
29mod discover;
30mod fingerprint;
31mod lakefile_toml;
32mod limits;
33mod loader;
34pub mod manifest_validation;
35mod modules;
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::{HOST_TRIPLE, LAKE_FIXTURE_DIGEST, ToolchainFingerprint};
46pub use lean_rs_sys::{LEAN_HEADER_DIGEST, LEAN_HEADER_PATH, LEAN_VERSION};
47pub use lean_rs_sys::{SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_by_digest, supported_for};
48pub use limits::{
49    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX, LEAN_HEARTBEAT_LIMIT_DEFAULT,
50    LEAN_HEARTBEAT_LIMIT_MAX,
51};
52pub use loader::{
53    LOADER_DIAGNOSTIC_TEXT_LIMIT, LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership, LeanExportResultConvention,
54    LeanExportReturnAbi, LeanExportSignature, LeanExportSymbolKind, LeanLibraryDependency, LeanLoaderCheck,
55    LeanLoaderDiagnosticCode, LeanLoaderReport, LeanLoaderSeverity, LeanModuleInitializer, bound_loader_text,
56};
57pub use manifest_validation::CapabilityManifest;
58pub use modules::{
59    LeanLakeProjectModules, LeanModuleDescriptor, LeanModuleDiscoveryDiagnostic, LeanModuleDiscoveryOptions,
60    LeanModuleSetFingerprint, discover_lake_modules,
61};
62
63/// Version of the `lean-toolchain` crate, matching `Cargo.toml`.
64pub const VERSION: &str = env!("CARGO_PKG_VERSION");
65
66/// Curated allowlist of `LEAN_EXPORT` symbols the workspace relies on.
67///
68/// Returns [`lean_rs_sys::REQUIRED_SYMBOLS`] directly—the allowlist lives in
69/// exactly one place. Use this through `lean-toolchain` so consumer crates do
70/// not also need a direct `lean-rs-sys` dependency just to enumerate symbol
71/// names.
72#[must_use]
73pub fn required_symbols() -> &'static [&'static str] {
74    lean_rs_sys::REQUIRED_SYMBOLS
75}
76
77#[cfg(test)]
78mod tests {
79    use super::{LEAN_HEADER_DIGEST, LEAN_VERSION, VERSION, required_symbols};
80
81    #[test]
82    fn version_constant_matches_package() {
83        assert_eq!(VERSION, env!("CARGO_PKG_VERSION"));
84    }
85
86    #[test]
87    fn required_symbols_is_nonempty() {
88        assert!(!required_symbols().is_empty());
89    }
90
91    #[test]
92    fn lean_metadata_is_baked() {
93        assert!(!LEAN_VERSION.is_empty());
94        assert_eq!(LEAN_HEADER_DIGEST.len(), 64);
95        assert!(LEAN_HEADER_DIGEST.chars().all(|c| c.is_ascii_hexdigit()));
96    }
97}
lean_toolchain/lib.rs

lean_toolchain/
lib.rs
