lean_toolchain/
discover.rs

1//! Typed Lean toolchain discovery.
2//!
3//! Probe precedence (first probe whose `<prefix>/include/lean/lean.h` exists wins):
4//!
5//! 1. `DiscoverOptions::explicit_sysroot`.
6//! 2. `$LEAN_SYSROOT`.
7//! 3. `$ELAN_HOME` + `elan show active-toolchain`.
8//! 4. `lean --print-prefix` (via `PATH`).
9//! 5. `lake env printenv LEAN_SYSROOT` under a workspace `fixtures/lean` directory.
10//!
11//! Each probe is independently gated by a `DiscoverOptions` flag so callers
12//! can lock down behaviour for reproducible builds.
13
14use std::env;
15use std::fs;
16use std::path::{Path, PathBuf};
17use std::process::Command;
18
19use crate::diagnostics::LinkDiagnostics;
20use crate::fingerprint::ToolchainFingerprint;
21
22/// Which probe produced the resolved toolchain.
23#[derive(Clone, Copy, Debug, Eq, PartialEq)]
24pub enum DiscoverySource {
25    /// Caller supplied `DiscoverOptions::explicit_sysroot`.
26    ExplicitSysroot,
27    /// Caller had `LEAN_SYSROOT` exported in the environment.
28    LeanSysrootEnv,
29    /// Resolved via `$ELAN_HOME` + `elan show active-toolchain`.
30    ElanHome,
31    /// Resolved via `lean --print-prefix` on `PATH`.
32    Path,
33    /// Resolved via `lake env printenv LEAN_SYSROOT` under a workspace fixture.
34    LakeFixtureEnv,
35}
36
37/// Knobs that gate which discovery probes run.
38///
39/// `Default` enables every probe; tests and reproducible builds narrow the
40/// set to produce deterministic behaviour.
41#[derive(Clone, Debug)]
42pub struct DiscoverOptions {
43    /// Caller-supplied sysroot; bypasses every other probe when set.
44    pub explicit_sysroot: Option<PathBuf>,
45    /// Consult `lean --print-prefix` (requires `lean` on `PATH`).
46    pub allow_path_lookup: bool,
47    /// Consult `$ELAN_HOME` + `elan show active-toolchain`.
48    pub allow_elan: bool,
49    /// Consult `lake env printenv LEAN_SYSROOT` under `fixtures/lean`.
50    pub allow_lake_env: bool,
51    /// Optional `lean-toolchain` file to parse for the recorded version.
52    pub toolchain_file: Option<PathBuf>,
53}
54
55impl Default for DiscoverOptions {
56    fn default() -> Self {
57        Self {
58            explicit_sysroot: None,
59            allow_path_lookup: true,
60            allow_elan: true,
61            allow_lake_env: true,
62            toolchain_file: None,
63        }
64    }
65}
66
67/// Outcome of a successful discovery.
68///
69/// `#[non_exhaustive]` so additional fields can be added without breaking
70/// downstream pattern-matchers.
71#[non_exhaustive]
72#[derive(Clone, Debug)]
73pub struct ToolchainInfo {
74    /// The discovered Lean prefix directory (`<prefix>/include/lean/lean.h` exists).
75    pub prefix: PathBuf,
76    /// `<prefix>/bin/lean` if present on disk.
77    pub lean_binary: Option<PathBuf>,
78    /// `<prefix>/include/lean/lean.h`.
79    pub header_path: PathBuf,
80    /// `<prefix>/lib`.
81    pub lib_dir: PathBuf,
82    /// Version string parsed at discovery time (from a `lean-toolchain` file,
83    /// `version.h`, or `lean --version`). Falls back to `LEAN_VERSION` from
84    /// `lean-rs-sys` when no live source is available.
85    pub version: String,
86    /// Build-baked fingerprint (does not vary with discovery results).
87    pub fingerprint: ToolchainFingerprint,
88    /// Which probe won.
89    pub source: DiscoverySource,
90}
91
92/// Resolve a Lean toolchain following the documented probe precedence.
93///
94/// # Errors
95///
96/// Returns `LinkDiagnostics::MissingLean { tried }` if no probe yields a
97/// directory containing `include/lean/lean.h`. Each entry in `tried` is one
98/// line describing why a probe was skipped or which path it inspected.
99pub fn discover_toolchain(opts: &DiscoverOptions) -> Result<ToolchainInfo, LinkDiagnostics> {
100    let mut tried: Vec<String> = Vec::new();
101
102    if let Some(sysroot) = opts.explicit_sysroot.as_ref() {
103        if has_header(sysroot) {
104            return Ok(build_info(sysroot.clone(), DiscoverySource::ExplicitSysroot, opts));
105        }
106        tried.push(format!(
107            "explicit_sysroot={} (no include/lean/lean.h)",
108            sysroot.display()
109        ));
110    } else {
111        tried.push("explicit_sysroot unset".into());
112    }
113
114    match env::var_os("LEAN_SYSROOT") {
115        Some(value) => {
116            let path = PathBuf::from(&value);
117            if has_header(&path) {
118                return Ok(build_info(path, DiscoverySource::LeanSysrootEnv, opts));
119            }
120            tried.push(format!("LEAN_SYSROOT={} (no include/lean/lean.h)", path.display()));
121        }
122        None => tried.push("LEAN_SYSROOT unset".into()),
123    }
124
125    if opts.allow_elan {
126        match elan_prefix() {
127            Ok(Some(path)) => {
128                if has_header(&path) {
129                    return Ok(build_info(path, DiscoverySource::ElanHome, opts));
130                }
131                tried.push(format!("elan toolchain {} (no include/lean/lean.h)", path.display()));
132            }
133            Ok(None) => tried.push("ELAN_HOME unset or elan unavailable".into()),
134            Err(reason) => tried.push(reason),
135        }
136    } else {
137        tried.push("elan probe disabled".into());
138    }
139
140    if opts.allow_path_lookup {
141        match lean_print_prefix() {
142            Ok(Some(path)) => {
143                if has_header(&path) {
144                    return Ok(build_info(path, DiscoverySource::Path, opts));
145                }
146                tried.push(format!(
147                    "`lean --print-prefix` = {} (no include/lean/lean.h)",
148                    path.display()
149                ));
150            }
151            Ok(None) => tried.push("`lean --print-prefix` returned nothing".into()),
152            Err(reason) => tried.push(reason),
153        }
154    } else {
155        tried.push("PATH lookup disabled".into());
156    }
157
158    if opts.allow_lake_env {
159        match lake_fixture_prefix() {
160            Ok(Some(path)) => {
161                if has_header(&path) {
162                    return Ok(build_info(path, DiscoverySource::LakeFixtureEnv, opts));
163                }
164                tried.push(format!(
165                    "lake fixture prefix {} (no include/lean/lean.h)",
166                    path.display()
167                ));
168            }
169            Ok(None) => tried.push("lake fixture probe: no workspace `fixtures/lean` found".into()),
170            Err(reason) => tried.push(reason),
171        }
172    } else {
173        tried.push("lake env probe disabled".into());
174    }
175
176    Err(LinkDiagnostics::MissingLean { tried })
177}
178
179fn has_header(prefix: &Path) -> bool {
180    prefix.join("include").join("lean").join("lean.h").is_file()
181}
182
183fn build_info(prefix: PathBuf, source: DiscoverySource, opts: &DiscoverOptions) -> ToolchainInfo {
184    let header_path = prefix.join("include").join("lean").join("lean.h");
185    let lib_dir = prefix.join("lib");
186    let lean_binary = {
187        let candidate = prefix.join("bin").join("lean");
188        if candidate.is_file() { Some(candidate) } else { None }
189    };
190    let version = opts
191        .toolchain_file
192        .as_deref()
193        .and_then(parse_toolchain_file)
194        .or_else(|| parse_version_header(&prefix))
195        .unwrap_or_else(|| lean_rs_sys::LEAN_VERSION.to_string());
196    ToolchainInfo {
197        prefix,
198        lean_binary,
199        header_path,
200        lib_dir,
201        version,
202        fingerprint: ToolchainFingerprint::current(),
203        source,
204    }
205}
206
207fn parse_toolchain_file(path: &Path) -> Option<String> {
208    let text = fs::read_to_string(path).ok()?;
209    // Expected shape: `leanprover/lean4:v4.X.Y` (single line). Any version
210    // string is accepted; the caller validates against the supported window.
211    let line = text.lines().next()?.trim();
212    let (_channel, tag) = line.split_once(':')?;
213    Some(tag.trim_start_matches('v').to_string())
214}
215
216fn parse_version_header(prefix: &Path) -> Option<String> {
217    let version_h = prefix.join("include").join("lean").join("version.h");
218    let text = fs::read_to_string(&version_h).ok()?;
219    for line in text.lines() {
220        if let Some(rest) = line.trim().strip_prefix("#define LEAN_VERSION_STRING") {
221            let trimmed = rest.trim().trim_matches('"');
222            if !trimmed.is_empty() {
223                return Some(trimmed.to_string());
224            }
225        }
226    }
227    None
228}
229
230fn elan_prefix() -> Result<Option<PathBuf>, String> {
231    let Some(elan_home) = env::var_os("ELAN_HOME") else {
232        return Ok(None);
233    };
234    let output = Command::new("elan")
235        .args(["show", "active-toolchain"])
236        .output()
237        .map_err(|err| format!("`elan show active-toolchain` failed: {err}"))?;
238    if !output.status.success() {
239        return Err(format!("`elan show active-toolchain` exited {}", output.status));
240    }
241    let toolchain = String::from_utf8_lossy(&output.stdout)
242        .lines()
243        .next()
244        .unwrap_or("")
245        .split_whitespace()
246        .next()
247        .unwrap_or("")
248        .to_string();
249    if toolchain.is_empty() {
250        return Ok(None);
251    }
252    Ok(Some(PathBuf::from(elan_home).join("toolchains").join(toolchain)))
253}
254
255fn lean_print_prefix() -> Result<Option<PathBuf>, String> {
256    let output = Command::new("lean")
257        .arg("--print-prefix")
258        .output()
259        .map_err(|err| format!("`lean --print-prefix` failed: {err}"))?;
260    if !output.status.success() {
261        return Err(format!("`lean --print-prefix` exited {}", output.status));
262    }
263    let prefix = String::from_utf8_lossy(&output.stdout).trim().to_string();
264    if prefix.is_empty() {
265        Ok(None)
266    } else {
267        Ok(Some(PathBuf::from(prefix)))
268    }
269}
270
271fn lake_fixture_prefix() -> Result<Option<PathBuf>, String> {
272    let Some(fixture_dir) = find_workspace_fixture() else {
273        return Ok(None);
274    };
275    let output = Command::new("lake")
276        .args(["env", "printenv", "LEAN_SYSROOT"])
277        .current_dir(&fixture_dir)
278        .output()
279        .map_err(|err| format!("`lake env printenv LEAN_SYSROOT` failed: {err}"))?;
280    if !output.status.success() {
281        return Err(format!("`lake env printenv LEAN_SYSROOT` exited {}", output.status));
282    }
283    let prefix = String::from_utf8_lossy(&output.stdout).trim().to_string();
284    if prefix.is_empty() {
285        Ok(None)
286    } else {
287        Ok(Some(PathBuf::from(prefix)))
288    }
289}
290
291fn find_workspace_fixture() -> Option<PathBuf> {
292    // CARGO_MANIFEST_DIR is set during cargo invocations (build + test); at
293    // arbitrary runtime we fall back to the current dir.
294    let start = env::var_os("CARGO_MANIFEST_DIR")
295        .map(PathBuf::from)
296        .or_else(|| env::current_dir().ok())?;
297    let mut cursor: &Path = start.as_path();
298    loop {
299        let candidate = cursor.join("fixtures").join("lean");
300        if candidate.join("lakefile.lean").is_file() {
301            return Some(candidate);
302        }
303        cursor = cursor.parent()?;
304    }
305}
lean_toolchain/discover.rs

lean_toolchain/
discover.rs
