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#[derive(Clone, Debug)]
69pub struct ToolchainInfo {
70    /// The discovered Lean prefix directory (`<prefix>/include/lean/lean.h` exists).
71    pub prefix: PathBuf,
72    /// `<prefix>/bin/lean` if present on disk.
73    pub lean_binary: Option<PathBuf>,
74    /// `<prefix>/include/lean/lean.h`.
75    pub header_path: PathBuf,
76    /// `<prefix>/lib`.
77    pub lib_dir: PathBuf,
78    /// Version string parsed at discovery time (from a `lean-toolchain` file,
79    /// `version.h`, or `lean --version`). Falls back to `LEAN_VERSION` from
80    /// `lean-rs-sys` when no live source is available.
81    pub version: String,
82    /// Build-baked fingerprint (does not vary with discovery results).
83    pub fingerprint: ToolchainFingerprint,
84    /// Which probe won.
85    pub source: DiscoverySource,
86}
87
88/// Resolve a Lean toolchain following the documented probe precedence.
89///
90/// # Errors
91///
92/// Returns `LinkDiagnostics::MissingLean { tried }` if no probe yields a
93/// directory containing `include/lean/lean.h`. Each entry in `tried` is one
94/// line describing why a probe was skipped or which path it inspected.
95pub fn discover_toolchain(opts: &DiscoverOptions) -> Result<ToolchainInfo, LinkDiagnostics> {
96    let mut tried: Vec<String> = Vec::new();
97
98    if let Some(sysroot) = opts.explicit_sysroot.as_ref() {
99        if has_header(sysroot) {
100            return Ok(build_info(sysroot.clone(), DiscoverySource::ExplicitSysroot, opts));
101        }
102        tried.push(format!(
103            "explicit_sysroot={} (no include/lean/lean.h)",
104            sysroot.display()
105        ));
106    } else {
107        tried.push("explicit_sysroot unset".into());
108    }
109
110    match env::var_os("LEAN_SYSROOT") {
111        Some(value) => {
112            let path = PathBuf::from(&value);
113            if has_header(&path) {
114                return Ok(build_info(path, DiscoverySource::LeanSysrootEnv, opts));
115            }
116            tried.push(format!("LEAN_SYSROOT={} (no include/lean/lean.h)", path.display()));
117        }
118        None => tried.push("LEAN_SYSROOT unset".into()),
119    }
120
121    if opts.allow_elan {
122        match elan_prefix() {
123            Ok(Some(path)) => {
124                if has_header(&path) {
125                    return Ok(build_info(path, DiscoverySource::ElanHome, opts));
126                }
127                tried.push(format!("elan toolchain {} (no include/lean/lean.h)", path.display()));
128            }
129            Ok(None) => tried.push("ELAN_HOME unset or elan unavailable".into()),
130            Err(reason) => tried.push(reason),
131        }
132    } else {
133        tried.push("elan probe disabled".into());
134    }
135
136    if opts.allow_path_lookup {
137        match lean_print_prefix() {
138            Ok(Some(path)) => {
139                if has_header(&path) {
140                    return Ok(build_info(path, DiscoverySource::Path, opts));
141                }
142                tried.push(format!(
143                    "`lean --print-prefix` = {} (no include/lean/lean.h)",
144                    path.display()
145                ));
146            }
147            Ok(None) => tried.push("`lean --print-prefix` returned nothing".into()),
148            Err(reason) => tried.push(reason),
149        }
150    } else {
151        tried.push("PATH lookup disabled".into());
152    }
153
154    if opts.allow_lake_env {
155        match lake_fixture_prefix() {
156            Ok(Some(path)) => {
157                if has_header(&path) {
158                    return Ok(build_info(path, DiscoverySource::LakeFixtureEnv, opts));
159                }
160                tried.push(format!(
161                    "lake fixture prefix {} (no include/lean/lean.h)",
162                    path.display()
163                ));
164            }
165            Ok(None) => tried.push("lake fixture probe: no workspace `fixtures/lean` found".into()),
166            Err(reason) => tried.push(reason),
167        }
168    } else {
169        tried.push("lake env probe disabled".into());
170    }
171
172    Err(LinkDiagnostics::MissingLean { tried })
173}
174
175fn has_header(prefix: &Path) -> bool {
176    prefix.join("include").join("lean").join("lean.h").is_file()
177}
178
179fn build_info(prefix: PathBuf, source: DiscoverySource, opts: &DiscoverOptions) -> ToolchainInfo {
180    let header_path = prefix.join("include").join("lean").join("lean.h");
181    let lib_dir = prefix.join("lib");
182    let lean_binary = {
183        let candidate = prefix.join("bin").join("lean");
184        if candidate.is_file() { Some(candidate) } else { None }
185    };
186    let version = opts
187        .toolchain_file
188        .as_deref()
189        .and_then(parse_toolchain_file)
190        .or_else(|| parse_version_header(&prefix))
191        .unwrap_or_else(|| lean_rs_sys::LEAN_VERSION.to_string());
192    ToolchainInfo {
193        prefix,
194        lean_binary,
195        header_path,
196        lib_dir,
197        version,
198        fingerprint: ToolchainFingerprint::current(),
199        source,
200    }
201}
202
203fn parse_toolchain_file(path: &Path) -> Option<String> {
204    let text = fs::read_to_string(path).ok()?;
205    // Expected shape: `leanprover/lean4:v4.X.Y` (single line). Any version
206    // string is accepted; the caller validates against the supported window.
207    let line = text.lines().next()?.trim();
208    let (_channel, tag) = line.split_once(':')?;
209    Some(tag.trim_start_matches('v').to_string())
210}
211
212fn parse_version_header(prefix: &Path) -> Option<String> {
213    let version_h = prefix.join("include").join("lean").join("version.h");
214    let text = fs::read_to_string(&version_h).ok()?;
215    for line in text.lines() {
216        if let Some(rest) = line.trim().strip_prefix("#define LEAN_VERSION_STRING") {
217            let trimmed = rest.trim().trim_matches('"');
218            if !trimmed.is_empty() {
219                return Some(trimmed.to_string());
220            }
221        }
222    }
223    None
224}
225
226fn elan_prefix() -> Result<Option<PathBuf>, String> {
227    let Some(elan_home) = env::var_os("ELAN_HOME") else {
228        return Ok(None);
229    };
230    let output = Command::new("elan")
231        .args(["show", "active-toolchain"])
232        .output()
233        .map_err(|err| format!("`elan show active-toolchain` failed: {err}"))?;
234    if !output.status.success() {
235        return Err(format!("`elan show active-toolchain` exited {}", output.status));
236    }
237    let toolchain = String::from_utf8_lossy(&output.stdout)
238        .lines()
239        .next()
240        .unwrap_or("")
241        .split_whitespace()
242        .next()
243        .unwrap_or("")
244        .to_string();
245    if toolchain.is_empty() {
246        return Ok(None);
247    }
248    Ok(Some(PathBuf::from(elan_home).join("toolchains").join(toolchain)))
249}
250
251fn lean_print_prefix() -> Result<Option<PathBuf>, String> {
252    let output = Command::new("lean")
253        .arg("--print-prefix")
254        .output()
255        .map_err(|err| format!("`lean --print-prefix` failed: {err}"))?;
256    if !output.status.success() {
257        return Err(format!("`lean --print-prefix` exited {}", output.status));
258    }
259    let prefix = String::from_utf8_lossy(&output.stdout).trim().to_string();
260    if prefix.is_empty() {
261        Ok(None)
262    } else {
263        Ok(Some(PathBuf::from(prefix)))
264    }
265}
266
267fn lake_fixture_prefix() -> Result<Option<PathBuf>, String> {
268    let Some(fixture_dir) = find_workspace_fixture() else {
269        return Ok(None);
270    };
271    let output = Command::new("lake")
272        .args(["env", "printenv", "LEAN_SYSROOT"])
273        .current_dir(&fixture_dir)
274        .output()
275        .map_err(|err| format!("`lake env printenv LEAN_SYSROOT` failed: {err}"))?;
276    if !output.status.success() {
277        return Err(format!("`lake env printenv LEAN_SYSROOT` exited {}", output.status));
278    }
279    let prefix = String::from_utf8_lossy(&output.stdout).trim().to_string();
280    if prefix.is_empty() {
281        Ok(None)
282    } else {
283        Ok(Some(PathBuf::from(prefix)))
284    }
285}
286
287fn find_workspace_fixture() -> Option<PathBuf> {
288    // CARGO_MANIFEST_DIR is set during cargo invocations (build + test); at
289    // arbitrary runtime we fall back to the current dir.
290    let start = env::var_os("CARGO_MANIFEST_DIR")
291        .map(PathBuf::from)
292        .or_else(|| env::current_dir().ok())?;
293    let mut cursor: &Path = start.as_path();
294    loop {
295        let candidate = cursor.join("fixtures").join("lean");
296        if candidate.join("lakefile.lean").is_file() {
297            return Some(candidate);
298        }
299        cursor = cursor.parent()?;
300    }
301}
lean_toolchain/discover.rs

lean_toolchain/
discover.rs
