Crate lean_toolchain 

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.

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.

LeanLakeProjectModules

A discovered Lake project and its Lean modules.

LeanModuleDescriptor

A discovered Lean source module in a Lake project.

LeanModuleDiscoveryOptions

Options for Lake module discovery.

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

DiscoverySource

Which probe produced the resolved toolchain.

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_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_VERSION

LEAN_VERSION_STRING as read from the active toolchain’s version.h (e.g. "4.29.1").

VERSION

Version of the lean-toolchain crate, matching Cargo.toml.

Functions

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.

lake_target_declared

Return whether a Lake lean_lib target is declared in a project.

required_symbols

Curated allowlist of LEAN_EXPORT symbols the workspace relies on.