Crate lean_toolchain

Expand description

Lean 4 toolchain discovery, fingerprinting, allowlist re-export, and build-script helpers.

Sits one layer above the workspace crate lean_rs_sys, which owns the raw extern "C" declarations, the hand-written refcount inline helpers, the signature-checked symbol allowlist, the header SHA-256 digest, and the link directives. This crate composes on top: a typed ToolchainFingerprint, the workspace-only Lake LAKE_FIXTURE_DIGEST, a layered LinkDiagnostics error type, and reusable build-script helpers (emit_lean_link_directives_checked, build_lake_target, build_lake_target_quiet) that downstream embedders and higher layers can use to get consistent link/rerun directives and Lake dylib paths without duplicating policy.

§Single typed entry point

LEAN_VERSION, LEAN_HEADER_PATH, and LEAN_HEADER_DIGEST are re-exported from lean_rs_sys so embedders that depend on this crate need only one import for build metadata. The allowlist comes through required_symbols (no copy).

§Layering

lean-rs-sys → lean-toolchain → lean-rs. Raw lean_* symbols never appear in this crate’s public surface — they remain in lean-rs-sys and reach the safe layers through lean-rs’s pub(crate) modules.

Re-exports§

pub use manifest_validation::CapabilityManifest;

Modules§

manifest_validation: Static, link-free validation of Lean capability manifests.

Structs§

BuiltLeanCapability: Metadata produced by CargoLeanCapability.
CargoLeanCapability: Build-script helper for shipping a Rust crate with bundled Lean code.
DiscoverOptions: Knobs that gate which discovery probes run.
LeanBuiltCapability: Runtime descriptor for a Lean capability built by a downstream build.rs.
LeanLakeProjectModules: A discovered Lake project and its Lean modules.
LeanLibraryDependency: Dependency dylib that must stay alive while a capability is loaded.
LeanLoaderCheck: One bounded preflight finding.
LeanLoaderReport: Structured result of loader preflight for one capability manifest.
LeanModuleDescriptor: A discovered Lean source module in a Lake project.
LeanModuleDiscoveryOptions: Options for Lake module discovery.
LeanModuleInitializer: Initializer for a Lean module hosted by a loaded dylib.
LeanModuleSetFingerprint: Stable facts about the discovered project source set.
ToolchainFingerprint: Typed identity of the Lean toolchain this crate was compiled against.
ToolchainInfo: Outcome of a successful discovery.

Enums§

BuiltCapabilityArtifact: Which artifact a LeanBuiltCapability resolution was looking for.
DiscoverySource: Which probe produced the resolved toolchain.
LeanBuiltCapabilityError: Errors returned when resolving a LeanBuiltCapability descriptor.
LeanLoaderDiagnosticCode: Stable preflight diagnostic codes for manifest-backed capability loading.
LeanLoaderSeverity: Severity of one loader preflight finding.
LeanModuleDiscoveryDiagnostic: Typed diagnostics for Lake module discovery.
LinkDiagnostics: Reasons the Lean toolchain or its linkage could not be resolved.

Constants§

CAPABILITY_MANIFEST_SCHEMA_VERSION: Current JSON schema version for CargoLeanCapability artifact manifests.
HOST_TRIPLE: Cargo TARGET triple lean-toolchain was built for.
LAKE_FIXTURE_DIGEST: SHA-256 over the workspace Lake fixture’s manifest plus compiled native artifacts.
LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT: Default byte budget for the diagnostic collection returned per call (64 KiB ≈ 16 default-bounded messages).
LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX: Upper bound on the diagnostic byte budget (1 MiB).
LEAN_HEADER_DIGEST: SHA-256 of the resolved lean.h. Computed by build.rs and equal to the header_digest of the matched SupportedToolchain entry.
LEAN_HEADER_PATH: Filesystem path to the lean.h that the build was resolved against.
LEAN_HEARTBEAT_LIMIT_DEFAULT: Default heartbeat ceiling — matches Lean’s own maxHeartbeats default at 4.29.1 (Lean.Core.maxHeartbeats).
LEAN_HEARTBEAT_LIMIT_MAX: Upper bound on the heartbeat ceiling. 1000× the default; values above saturate at this ceiling so a runaway elaborator finishes in bounded real time on every supported host.
LEAN_VERSION: LEAN_VERSION_STRING as read from the active toolchain’s version.h (e.g. "4.29.1").
LOADER_DIAGNOSTIC_TEXT_LIMIT: Maximum bytes preserved in user-facing loader diagnostic strings.
VERSION: Version of the lean-toolchain crate, matching Cargo.toml.

Functions§

bound_loader_text: Truncate text to at most LOADER_DIAGNOSTIC_TEXT_LIMIT bytes on a UTF-8 char boundary.
build_lake_target: Build a Lake lean_lib shared-library target and return the produced dylib path.
build_lake_target_quiet: Build a Lake lean_lib shared-library target without emitting Cargo build-script directives.
capability_env_var: Default Cargo environment variable for a Lean capability target.
capability_manifest_env_var: Default Cargo environment variable for a Lean capability artifact manifest.
discover_lake_modules: Discover Lean modules in a Lake project.
discover_toolchain: Resolve a Lean toolchain following the documented probe precedence.
emit_lean_link_directives: Emit Lean link-search, link-lib, and runtime rpath directives plus matching rerun triggers from a downstream build.rs.
emit_lean_link_directives_checked: Emit Lean link-search, link-lib, and runtime rpath directives, returning typed diagnostics if the active Lean toolchain cannot be resolved.
required_symbols: Curated allowlist of LEAN_EXPORT symbols the workspace relies on.