Skip to main content

discover_toolchain

lean_toolchain

Function discover_toolchain 

Source 
pub fn discover_toolchain(
    opts: &DiscoverOptions,
) -> Result<ToolchainInfo, LinkDiagnostics>
Expand description

Resolve a Lean toolchain following the documented probe precedence.

ยงErrors

Returns LinkDiagnostics::MissingLean { tried } if no probe yields a directory containing include/lean/lean.h. Each entry in tried is one line describing why a probe was skipped or which path it inspected.