Crate lean_toolchain

Expand description

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

Sits one layer above lean_rs_abi, which owns link-free ABI/toolchain metadata. 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, LEAN_HEADER_DIGEST, and LEAN_RESOLVED_VERSION are resolved by this crate’s build.rs (probing the active toolchain, degrading to the latest supported entry when none is installed), so embedders need only one import for build metadata. Live toolchain identity lives here, not in lean_rs_abi, which is purely static. The allowlist comes through required_symbols (no copy).

§Layering

lean-rs-abi → lean-toolchain for link-free metadata, and lean-rs-sys → lean-rs for raw runtime FFI. Raw lean_* symbols never appear in this crate’s public surface.

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.
GeneratedSourceFile: Source-root-relative generated file written during materialization.
LeanBuiltCapability: Runtime descriptor for a Lean capability built by a downstream build.rs.
LeanExportArgAbi: ABI shape of one exported function argument.
LeanExportReturnAbi: ABI shape of an exported result.
LeanExportSignature: Trusted manifest signature for one Lean export.
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.
MaterializedSourcePackage: Materialized source package.
SourcePackageMaterializationRequest: Request to materialize a package-owned Lean source payload.
SourcePackageProvenance: Provenance sidecar for a materialized source package.
SupportedToolchain: One ABI-equivalence class in the supported toolchain window.
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.
LeanExportAbiRepr: C ABI representation for one exported argument or result slot.
LeanExportOwnership: Ownership convention for one ABI slot.
LeanExportResultConvention: How an exported result is decoded.
LeanExportSymbolKind: Whether an exported symbol is callable code or a Lean persistent global.
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.
SourcePackageError: Source package materialization errors.
SourcePackageManifestPolicy: Validation policy for the materialized lake-manifest.json.

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, lowercase hex.
LEAN_HEADER_PATH: Filesystem path to the lean.h this build resolved against, or a sentinel on a metadata-only build with no toolchain present.
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_RESOLVED_VERSION: Version string from the matched supported-toolchain entry (equal to LEAN_VERSION except when several releases share one lean.h).
LEAN_VERSION: LEAN_VERSION_STRING read from the active toolchain’s version.h, or the latest supported version on a metadata-only build with no toolchain present.
LOADER_DIAGNOSTIC_TEXT_LIMIT: Maximum bytes preserved in user-facing loader diagnostic strings.
SUPPORTED_TOOLCHAINS: The supported Lean toolchain window.
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.
materialize_source_package: Materialize a package-owned Lean source payload into a digest-keyed cache.
required_symbols: Curated allowlist of LEAN_EXPORT symbols the workspace relies on.
supported_by_digest: Return the SupportedToolchain entry whose header_digest matches the given lowercase-hex SHA-256 string, if any.
supported_for: Return the SupportedToolchain entry that includes version, if any.