lean_toolchain/
modules.rs

1//! Lake project module discovery for higher-level planners.
2//!
3//! This module knows Lake source layout and module-name validation. It does
4//! not know worker pools, downstream command names, or cache policy.
5
6use std::fmt;
7use std::fs;
8use std::path::{Path, PathBuf};
9use std::time::UNIX_EPOCH;
10
11use sha2::{Digest, Sha256};
12
13use crate::ToolchainFingerprint;
14use crate::lakefile_toml::parse_lakefile_toml;
15
16/// A discovered Lean source module in a Lake project.
17#[derive(Clone, Debug, Eq, PartialEq)]
18pub struct LeanModuleDescriptor {
19    pub module: String,
20    pub path: PathBuf,
21    pub source_root: String,
22}
23
24/// Stable facts about the discovered project source set.
25#[derive(Clone, Debug, Eq, PartialEq)]
26pub struct LeanModuleSetFingerprint {
27    pub toolchain: ToolchainFingerprint,
28    pub lakefile_sha256: String,
29    pub manifest_sha256: Option<String>,
30    pub source_count: u64,
31    pub source_max_mtime_ns: u128,
32}
33
34/// A discovered Lake project and its Lean modules.
35#[derive(Clone, Debug, Eq, PartialEq)]
36pub struct LeanLakeProjectModules {
37    pub requested_root: PathBuf,
38    pub project_root: PathBuf,
39    pub lakefile: PathBuf,
40    /// Lakefile-declared `lean_lib` target names, in lexicographic order.
41    ///
42    /// Empty when the lakefile declares no `lean_lib` targets. Distinct from
43    /// `module_roots`, which falls back to discovering top-level `*.lean` files
44    /// when no declaration is found. Callers verifying that a build target was
45    /// explicitly declared must consult this field, not `module_roots`.
46    pub declared_lean_libs: Vec<String>,
47    pub module_roots: Vec<String>,
48    pub selected_roots: Vec<String>,
49    pub modules: Vec<LeanModuleDescriptor>,
50    pub fingerprint: LeanModuleSetFingerprint,
51}
52
53/// Options for Lake module discovery.
54#[derive(Clone, Debug, Eq, PartialEq)]
55pub struct LeanModuleDiscoveryOptions {
56    requested_root: PathBuf,
57    selected_roots: Option<Vec<String>>,
58    toolchain: ToolchainFingerprint,
59}
60
61impl LeanModuleDiscoveryOptions {
62    /// Discover modules for the Lake project at or below `requested_root`.
63    #[must_use]
64    pub fn new(requested_root: impl Into<PathBuf>) -> Self {
65        Self {
66            requested_root: requested_root.into(),
67            selected_roots: None,
68            toolchain: ToolchainFingerprint::current(),
69        }
70    }
71
72    /// Restrict discovery to these Lake module roots.
73    #[must_use]
74    pub fn selected_roots(mut self, roots: impl IntoIterator<Item = impl Into<String>>) -> Self {
75        self.selected_roots = Some(roots.into_iter().map(Into::into).collect());
76        self
77    }
78
79    /// Override the toolchain fingerprint used for validation and fingerprints.
80    ///
81    /// This is primarily useful for tests and external planners that compare
82    /// a separately obtained toolchain identity.
83    #[must_use]
84    pub fn toolchain(mut self, toolchain: ToolchainFingerprint) -> Self {
85        self.toolchain = toolchain;
86        self
87    }
88}
89
90/// Typed diagnostics for Lake module discovery.
91#[derive(Debug)]
92pub enum LeanModuleDiscoveryDiagnostic {
93    MissingLakeRoot {
94        requested_root: PathBuf,
95    },
96    MissingModuleRoot {
97        project_root: PathBuf,
98        module_root: String,
99    },
100    InvalidModuleName {
101        module: String,
102        reason: String,
103    },
104    UnsupportedToolchain {
105        active: String,
106        supported_window: String,
107    },
108    Io {
109        path: PathBuf,
110        message: &'static str,
111        source: std::io::Error,
112    },
113}
114
115impl fmt::Display for LeanModuleDiscoveryDiagnostic {
116    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
117        match self {
118            Self::MissingLakeRoot { requested_root } => {
119                write!(
120                    f,
121                    "lean-toolchain: no Lake project found at {} or {}/lean",
122                    requested_root.display(),
123                    requested_root.display()
124                )
125            }
126            Self::MissingModuleRoot {
127                project_root,
128                module_root,
129            } => {
130                write!(
131                    f,
132                    "lean-toolchain: module root `{module_root}` was not found in {}",
133                    project_root.display()
134                )
135            }
136            Self::InvalidModuleName { module, reason } => {
137                write!(f, "lean-toolchain: invalid Lean module name `{module}`: {reason}")
138            }
139            Self::UnsupportedToolchain {
140                active,
141                supported_window,
142            } => {
143                write!(
144                    f,
145                    "lean-toolchain: active Lean toolchain {active} is not in the supported window: {supported_window}"
146                )
147            }
148            Self::Io { path, message, source } => {
149                write!(f, "lean-toolchain: {message} at {}: {source}", path.display())
150            }
151        }
152    }
153}
154
155impl std::error::Error for LeanModuleDiscoveryDiagnostic {
156    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
157        match self {
158            Self::Io { source, .. } => Some(source),
159            Self::MissingLakeRoot { .. }
160            | Self::MissingModuleRoot { .. }
161            | Self::InvalidModuleName { .. }
162            | Self::UnsupportedToolchain { .. } => None,
163        }
164    }
165}
166
167/// Discover Lean modules in a Lake project.
168///
169/// # Errors
170///
171/// Returns typed diagnostics when the Lake root cannot be found, the active
172/// toolchain is unsupported, a selected module root is missing, a module name
173/// cannot be represented safely, or source traversal fails.
174pub fn discover_lake_modules(
175    options: LeanModuleDiscoveryOptions,
176) -> Result<LeanLakeProjectModules, LeanModuleDiscoveryDiagnostic> {
177    if !options.toolchain.is_supported() {
178        return Err(LeanModuleDiscoveryDiagnostic::UnsupportedToolchain {
179            active: options.toolchain.lean_version.to_owned(),
180            supported_window: supported_window(),
181        });
182    }
183
184    let requested_root = normalize_existing(&options.requested_root)?;
185    let (project_root, lakefile) = lake_root_for(&requested_root)?;
186    let (declared_lean_libs, module_roots) = discover_module_roots(&project_root, &lakefile)?;
187    let selected_roots = options.selected_roots.unwrap_or_else(|| module_roots.clone());
188    for root in &selected_roots {
189        validate_module_name(root)?;
190        if !module_root_exists(&project_root, root) {
191            return Err(LeanModuleDiscoveryDiagnostic::MissingModuleRoot {
192                project_root,
193                module_root: root.clone(),
194            });
195        }
196    }
197
198    let modules = enumerate_sources(&project_root, &selected_roots)?;
199    let fingerprint = fingerprint_source_set(&project_root, &lakefile, &modules, options.toolchain)?;
200    Ok(LeanLakeProjectModules {
201        requested_root,
202        project_root,
203        lakefile,
204        declared_lean_libs,
205        module_roots,
206        selected_roots,
207        modules,
208        fingerprint,
209    })
210}
211
212fn normalize_existing(path: &Path) -> Result<PathBuf, LeanModuleDiscoveryDiagnostic> {
213    let expanded = expand_home(path);
214    if !expanded.exists() {
215        return Err(LeanModuleDiscoveryDiagnostic::MissingLakeRoot {
216            requested_root: expanded,
217        });
218    }
219    fs::canonicalize(&expanded).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
220        path: expanded,
221        message: "could not canonicalize path",
222        source,
223    })
224}
225
226fn expand_home(path: &Path) -> PathBuf {
227    let Some(text) = path.to_str() else {
228        return path.to_path_buf();
229    };
230    if text == "~" {
231        return home_dir().unwrap_or_else(|| path.to_path_buf());
232    }
233    if let Some(rest) = text.strip_prefix("~/")
234        && let Some(home) = home_dir()
235    {
236        return home.join(rest);
237    }
238    path.to_path_buf()
239}
240
241fn home_dir() -> Option<PathBuf> {
242    std::env::var_os("HOME").map(PathBuf::from)
243}
244
245fn lake_root_for(path: &Path) -> Result<(PathBuf, PathBuf), LeanModuleDiscoveryDiagnostic> {
246    if let Some(lakefile) = lakefile_path(path) {
247        return Ok((path.to_path_buf(), lakefile));
248    }
249    let nested = path.join("lean");
250    if let Some(lakefile) = lakefile_path(&nested) {
251        return Ok((nested, lakefile));
252    }
253    Err(LeanModuleDiscoveryDiagnostic::MissingLakeRoot {
254        requested_root: path.to_path_buf(),
255    })
256}
257
258fn lakefile_path(root: &Path) -> Option<PathBuf> {
259    let toml = root.join("lakefile.toml");
260    if toml.is_file() {
261        return Some(toml);
262    }
263    let lean = root.join("lakefile.lean");
264    lean.is_file().then_some(lean)
265}
266
267/// Parse the lakefile to learn what targets it declares, then decide what to walk.
268///
269/// Returns `(declared_lean_libs, module_roots)`:
270/// - `declared_lean_libs` is exactly the set of `lean_lib` targets named in the
271///   lakefile (Lean DSL or TOML). Empty when none are declared.
272/// - `module_roots` is the set the source walker uses: it equals
273///   `declared_lean_libs` when non-empty, or falls back to top-level `*.lean`
274///   stems so loose-script projects can still enumerate sources.
275///
276/// The two lists are deliberately distinct: a caller verifying that a build
277/// target was *explicitly* declared must use `declared_lean_libs`, because the
278/// top-level fallback can promote any `Foo.lean` at the project root into
279/// `module_roots` without Lake knowing it exists.
280fn discover_module_roots(
281    project_root: &Path,
282    lakefile: &Path,
283) -> Result<(Vec<String>, Vec<String>), LeanModuleDiscoveryDiagnostic> {
284    let mut declared = if lakefile.file_name().and_then(|name| name.to_str()) == Some("lakefile.toml") {
285        discover_toml_lakefile_roots(lakefile)?
286    } else {
287        discover_lean_lakefile_roots(lakefile)?
288    };
289    declared.sort();
290    declared.dedup();
291    for root in &declared {
292        validate_module_name(root)?;
293    }
294
295    let module_roots = if declared.is_empty() {
296        let mut fallback = discover_top_level_roots(project_root)?;
297        fallback.sort();
298        fallback.dedup();
299        for root in &fallback {
300            validate_module_name(root)?;
301        }
302        fallback
303    } else {
304        declared.clone()
305    };
306
307    Ok((declared, module_roots))
308}
309
310fn discover_toml_lakefile_roots(lakefile: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
311    let text = read_to_string(lakefile, "could not read Lake TOML file")?;
312    let parsed = parse_lakefile_toml(&text).map_err(|err| LeanModuleDiscoveryDiagnostic::Io {
313        path: lakefile.to_path_buf(),
314        message: "could not parse Lake TOML file",
315        source: std::io::Error::other(err.to_string()),
316    })?;
317    Ok(parsed.lean_libs)
318}
319
320fn discover_lean_lakefile_roots(lakefile: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
321    let text = read_to_string(lakefile, "could not read Lake file")?;
322    Ok(text
323        .lines()
324        .filter_map(|line| {
325            let trimmed = line.trim_start();
326            let rest = trimmed.strip_prefix("lean_lib ")?;
327            let raw = rest.split_whitespace().next()?;
328            let root = normalize_lake_identifier(raw);
329            (!root.is_empty()).then_some(root)
330        })
331        .collect())
332}
333
334fn discover_top_level_roots(project_root: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
335    let mut roots = Vec::new();
336    for entry in fs::read_dir(project_root).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
337        path: project_root.to_path_buf(),
338        message: "could not read Lake project directory",
339        source,
340    })? {
341        let entry = entry.map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
342            path: project_root.to_path_buf(),
343            message: "could not read Lake project directory entry",
344            source,
345        })?;
346        let path = entry.path();
347        if path.extension().and_then(|extension| extension.to_str()) == Some("lean")
348            && let Some(stem) = path.file_stem().and_then(|stem| stem.to_str())
349        {
350            roots.push(stem.to_owned());
351        }
352    }
353    Ok(roots)
354}
355
356fn module_root_exists(project_root: &Path, module_root: &str) -> bool {
357    module_to_file(project_root, module_root).is_file() || module_to_dir(project_root, module_root).is_dir()
358}
359
360fn enumerate_sources(
361    project_root: &Path,
362    selected_roots: &[String],
363) -> Result<Vec<LeanModuleDescriptor>, LeanModuleDiscoveryDiagnostic> {
364    let mut modules = std::collections::BTreeMap::<String, LeanModuleDescriptor>::new();
365    for source_root in selected_roots {
366        let root_file = module_to_file(project_root, source_root);
367        if root_file.is_file() {
368            modules.insert(
369                source_root.clone(),
370                LeanModuleDescriptor {
371                    module: source_root.clone(),
372                    path: root_file,
373                    source_root: source_root.clone(),
374                },
375            );
376        }
377
378        let module_dir = module_to_dir(project_root, source_root);
379        if module_dir.is_dir() {
380            collect_sources(project_root, &module_dir, source_root, &mut modules)?;
381        }
382    }
383    Ok(modules.into_values().collect())
384}
385
386fn collect_sources(
387    project_root: &Path,
388    dir: &Path,
389    source_root: &str,
390    modules: &mut std::collections::BTreeMap<String, LeanModuleDescriptor>,
391) -> Result<(), LeanModuleDiscoveryDiagnostic> {
392    for entry in fs::read_dir(dir).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
393        path: dir.to_path_buf(),
394        message: "could not read Lean source directory",
395        source,
396    })? {
397        let entry = entry.map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
398            path: dir.to_path_buf(),
399            message: "could not read Lean source directory entry",
400            source,
401        })?;
402        let path = entry.path();
403        let metadata = entry.metadata().map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
404            path: path.clone(),
405            message: "could not stat Lean source path",
406            source,
407        })?;
408        if metadata.is_dir() {
409            collect_sources(project_root, &path, source_root, modules)?;
410        } else if path.extension().and_then(|extension| extension.to_str()) == Some("lean") {
411            let module = module_from_path(project_root, &path)?;
412            validate_module_name(&module)?;
413            modules.insert(
414                module.clone(),
415                LeanModuleDescriptor {
416                    module,
417                    path,
418                    source_root: source_root.to_owned(),
419                },
420            );
421        }
422    }
423    Ok(())
424}
425
426fn fingerprint_source_set(
427    project_root: &Path,
428    lakefile: &Path,
429    modules: &[LeanModuleDescriptor],
430    toolchain: ToolchainFingerprint,
431) -> Result<LeanModuleSetFingerprint, LeanModuleDiscoveryDiagnostic> {
432    let lakefile_sha256 = sha256_file(lakefile)?;
433    let manifest = project_root.join("lake-manifest.json");
434    let manifest_sha256 = if manifest.is_file() {
435        Some(sha256_file(&manifest)?)
436    } else {
437        None
438    };
439    let mut source_max_mtime_ns = 0_u128;
440    for module in modules {
441        let metadata = fs::metadata(&module.path).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
442            path: module.path.clone(),
443            message: "could not stat Lean module source",
444            source,
445        })?;
446        let modified = metadata
447            .modified()
448            .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
449                path: module.path.clone(),
450                message: "could not read Lean module source mtime",
451                source,
452            })?;
453        let mtime_ns = modified
454            .duration_since(UNIX_EPOCH)
455            .map_or(0, |duration| duration.as_nanos());
456        source_max_mtime_ns = source_max_mtime_ns.max(mtime_ns);
457    }
458    Ok(LeanModuleSetFingerprint {
459        toolchain,
460        lakefile_sha256,
461        manifest_sha256,
462        source_count: modules.len() as u64,
463        source_max_mtime_ns,
464    })
465}
466
467fn sha256_file(path: &Path) -> Result<String, LeanModuleDiscoveryDiagnostic> {
468    fs::read(path)
469        .map(|bytes| sha256_hex(&bytes))
470        .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
471            path: path.to_path_buf(),
472            message: "could not read file for fingerprinting",
473            source,
474        })
475}
476
477fn sha256_hex(bytes: &[u8]) -> String {
478    let mut hasher = Sha256::new();
479    hasher.update(bytes);
480    let digest = hasher.finalize();
481    let mut out = String::with_capacity(digest.len().saturating_mul(2));
482    for byte in digest {
483        use std::fmt::Write as _;
484        if write!(out, "{byte:02x}").is_err() {
485            return out;
486        }
487    }
488    out
489}
490
491fn module_from_path(project_root: &Path, path: &Path) -> Result<String, LeanModuleDiscoveryDiagnostic> {
492    let relative = path
493        .strip_prefix(project_root)
494        .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
495            path: path.to_path_buf(),
496            message: "could not relativize Lean source path",
497            source: std::io::Error::other(source),
498        })?;
499    let mut parts: Vec<String> = relative
500        .components()
501        .map(|component| component.as_os_str().to_string_lossy().into_owned())
502        .collect();
503    if let Some(last) = parts.last_mut()
504        && let Some(stripped) = last.strip_suffix(".lean")
505    {
506        *last = stripped.to_owned();
507    }
508    Ok(parts.join("."))
509}
510
511fn module_to_file(project_root: &Path, module: &str) -> PathBuf {
512    let mut path = module_to_dir(project_root, module);
513    path.set_extension("lean");
514    path
515}
516
517fn module_to_dir(project_root: &Path, module: &str) -> PathBuf {
518    let mut path = project_root.to_path_buf();
519    for part in module.split('.') {
520        path.push(part);
521    }
522    path
523}
524
525fn normalize_lake_identifier(raw: &str) -> String {
526    raw.trim()
527        .trim_matches('`')
528        .trim_matches('«')
529        .trim_matches('»')
530        .trim_matches('"')
531        .trim()
532        .to_owned()
533}
534
535fn validate_module_name(module: &str) -> Result<(), LeanModuleDiscoveryDiagnostic> {
536    if module.is_empty() {
537        return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
538            module: module.to_owned(),
539            reason: "module name is empty".to_owned(),
540        });
541    }
542    for component in module.split('.') {
543        if component.is_empty() {
544            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
545                module: module.to_owned(),
546                reason: "module name contains an empty component".to_owned(),
547            });
548        }
549        let mut chars = component.chars();
550        let Some(first) = chars.next() else {
551            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
552                module: module.to_owned(),
553                reason: "module name contains an empty component".to_owned(),
554            });
555        };
556        if !(first == '_' || first.is_alphabetic()) {
557            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
558                module: module.to_owned(),
559                reason: "module components must begin with a letter or underscore".to_owned(),
560            });
561        }
562        if chars.any(|ch| !(ch == '_' || ch == '\'' || ch.is_alphanumeric())) {
563            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
564                module: module.to_owned(),
565                reason: "module components may contain only letters, digits, underscores, or apostrophes".to_owned(),
566            });
567        }
568    }
569    Ok(())
570}
571
572fn read_to_string(path: &Path, message: &'static str) -> Result<String, LeanModuleDiscoveryDiagnostic> {
573    fs::read_to_string(path).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
574        path: path.to_path_buf(),
575        message,
576        source,
577    })
578}
579
580fn supported_window() -> String {
581    lean_rs_sys::SUPPORTED_TOOLCHAINS
582        .iter()
583        .map(|entry| format!("{:?}", entry.versions))
584        .collect::<Vec<_>>()
585        .join(", ")
586}
587
588#[cfg(test)]
589#[allow(
590    clippy::expect_used,
591    clippy::panic,
592    clippy::unwrap_used,
593    clippy::wildcard_enum_match_arm
594)]
595mod tests {
596    use super::{LeanModuleDiscoveryDiagnostic, LeanModuleDiscoveryOptions, discover_lake_modules};
597    use crate::ToolchainFingerprint;
598    use std::fs;
599    use std::path::{Path, PathBuf};
600
601    #[test]
602    fn discovers_lean_lakefile_modules_deterministically() {
603        let root = temp_project("lean-lakefile");
604        write_file(&root.join("lakefile.lean"), "package demo\nlean_lib Demo where\n");
605        write_file(&root.join("Demo.lean"), "#check Nat\n");
606        fs::create_dir(root.join("Demo")).unwrap();
607        write_file(&root.join("Demo").join("B.lean"), "#check String\n");
608
609        let first = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
610        let second = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
611
612        assert_eq!(first.modules, second.modules);
613        assert_eq!(module_names(&first), vec!["Demo", "Demo.B"]);
614        assert_eq!(first.module_roots, vec!["Demo"]);
615        assert_eq!(first.fingerprint.source_count, 2);
616    }
617
618    #[test]
619    fn discovers_toml_lakefile_roots() {
620        let root = temp_project("toml-lakefile");
621        write_file(
622            &root.join("lakefile.toml"),
623            r#"
624name = "demo"
625[[lean_lib]]
626name = "Demo"
627[[lean_lib]]
628name = "Other"
629"#,
630        );
631        write_file(&root.join("Demo.lean"), "#check Nat\n");
632        write_file(&root.join("Other.lean"), "#check String\n");
633
634        let project = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
635        assert_eq!(project.module_roots, vec!["Demo", "Other"]);
636        assert_eq!(module_names(&project), vec!["Demo", "Other"]);
637    }
638
639    #[test]
640    fn missing_selected_root_is_typed() {
641        let root = temp_project("missing-root");
642        write_file(&root.join("lakefile.lean"), "package demo\nlean_lib Demo where\n");
643        write_file(&root.join("Demo.lean"), "#check Nat\n");
644
645        let err = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root).selected_roots(["Missing"]))
646            .expect_err("missing selected root should be typed");
647        match err {
648            LeanModuleDiscoveryDiagnostic::MissingModuleRoot { module_root, .. } => {
649                assert_eq!(module_root, "Missing");
650            }
651            other => panic!("expected missing module root, got {other:?}"),
652        }
653    }
654
655    #[test]
656    fn invalid_module_name_is_typed() {
657        let root = temp_project("invalid-module");
658        write_file(&root.join("lakefile.lean"), "package demo\nlean_lib Demo-Bad where\n");
659        write_file(&root.join("Demo-Bad.lean"), "#check Nat\n");
660
661        let err = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root))
662            .expect_err("invalid Lake module name should be typed");
663        match err {
664            LeanModuleDiscoveryDiagnostic::InvalidModuleName { module, .. } => {
665                assert_eq!(module, "Demo-Bad");
666            }
667            other => panic!("expected invalid module name, got {other:?}"),
668        }
669    }
670
671    #[test]
672    fn unsupported_toolchain_is_typed() {
673        let root = temp_project("unsupported-toolchain");
674        write_file(&root.join("lakefile.lean"), "package demo\nlean_lib Demo where\n");
675        write_file(&root.join("Demo.lean"), "#check Nat\n");
676        let mut fingerprint = ToolchainFingerprint::current();
677        fingerprint.lean_version = "0.0.0-test";
678
679        let err = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root).toolchain(fingerprint))
680            .expect_err("unsupported toolchain should be typed");
681        assert!(matches!(
682            err,
683            LeanModuleDiscoveryDiagnostic::UnsupportedToolchain { .. }
684        ));
685    }
686
687    #[test]
688    fn declared_lean_libs_reflects_lakefile() {
689        let root = temp_project("declared-lean-libs");
690        write_file(
691            &root.join("lakefile.lean"),
692            "package demo\nlean_lib Demo where\nlean_lib Extra where\n",
693        );
694        write_file(&root.join("Demo.lean"), "#check Nat\n");
695        write_file(&root.join("Extra.lean"), "#check Nat\n");
696
697        let project = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
698        assert_eq!(project.declared_lean_libs, vec!["Demo", "Extra"]);
699    }
700
701    #[test]
702    fn declared_lean_libs_reflects_toml_lakefile() {
703        let root = temp_project("declared-toml-libs");
704        write_file(
705            &root.join("lakefile.toml"),
706            r#"
707name = "demo"
708[[lean_lib]]
709name = "KanProofs"
710[[lean_lib]]
711name = "Other"
712"#,
713        );
714        write_file(&root.join("KanProofs.lean"), "#check Nat\n");
715        write_file(&root.join("Other.lean"), "#check Nat\n");
716
717        let project = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
718        assert_eq!(project.declared_lean_libs, vec!["KanProofs", "Other"]);
719    }
720
721    #[test]
722    fn declared_lean_libs_empty_when_top_level_fallback_active() {
723        // A project with loose top-level `*.lean` files but no `lean_lib`
724        // declaration must report `declared_lean_libs` as empty, so callers
725        // verifying explicit target declaration can reject this case before
726        // attempting a Lake build.
727        let root = temp_project("declared-fallback");
728        write_file(&root.join("lakefile.lean"), "package demo\n");
729        write_file(&root.join("Loose.lean"), "#check Nat\n");
730
731        let project = discover_lake_modules(LeanModuleDiscoveryOptions::new(&root)).unwrap();
732        assert!(project.declared_lean_libs.is_empty());
733        assert!(project.module_roots.iter().any(|root| root == "Loose"));
734    }
735
736    fn module_names(project: &super::LeanLakeProjectModules) -> Vec<&str> {
737        project.modules.iter().map(|module| module.module.as_str()).collect()
738    }
739
740    fn temp_project(name: &str) -> PathBuf {
741        let root = std::env::temp_dir().join(format!("lean-toolchain-modules-{name}-{}", std::process::id()));
742        if root.exists() {
743            fs::remove_dir_all(&root).unwrap();
744        }
745        fs::create_dir_all(&root).unwrap();
746        root
747    }
748
749    fn write_file(path: &Path, contents: &str) {
750        if let Some(parent) = path.parent() {
751            fs::create_dir_all(parent).unwrap();
752        }
753        fs::write(path, contents).unwrap();
754    }
755}
lean_toolchain/modules.rs

lean_toolchain/
modules.rs
