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

lean_toolchain/
modules.rs
