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    pub module_roots: Vec<String>,
40    pub selected_roots: Vec<String>,
41    pub modules: Vec<LeanModuleDescriptor>,
42    pub fingerprint: LeanModuleSetFingerprint,
43}
44
45/// Options for Lake module discovery.
46#[derive(Clone, Debug, Eq, PartialEq)]
47pub struct LeanModuleDiscoveryOptions {
48    requested_root: PathBuf,
49    selected_roots: Option<Vec<String>>,
50    toolchain: ToolchainFingerprint,
51}
52
53impl LeanModuleDiscoveryOptions {
54    /// Discover modules for the Lake project at or below `requested_root`.
55    #[must_use]
56    pub fn new(requested_root: impl Into<PathBuf>) -> Self {
57        Self {
58            requested_root: requested_root.into(),
59            selected_roots: None,
60            toolchain: ToolchainFingerprint::current(),
61        }
62    }
63
64    /// Restrict discovery to these Lake module roots.
65    #[must_use]
66    pub fn selected_roots(mut self, roots: impl IntoIterator<Item = impl Into<String>>) -> Self {
67        self.selected_roots = Some(roots.into_iter().map(Into::into).collect());
68        self
69    }
70
71    /// Override the toolchain fingerprint used for validation and fingerprints.
72    ///
73    /// This is primarily useful for tests and external planners that compare
74    /// a separately obtained toolchain identity.
75    #[must_use]
76    pub fn toolchain(mut self, toolchain: ToolchainFingerprint) -> Self {
77        self.toolchain = toolchain;
78        self
79    }
80}
81
82/// Typed diagnostics for Lake module discovery.
83#[non_exhaustive]
84#[derive(Debug)]
85pub enum LeanModuleDiscoveryDiagnostic {
86    MissingLakeRoot {
87        requested_root: PathBuf,
88    },
89    MissingModuleRoot {
90        project_root: PathBuf,
91        module_root: String,
92    },
93    InvalidModuleName {
94        module: String,
95        reason: String,
96    },
97    UnsupportedToolchain {
98        active: String,
99        supported_window: String,
100    },
101    Io {
102        path: PathBuf,
103        message: &'static str,
104        source: std::io::Error,
105    },
106}
107
108impl fmt::Display for LeanModuleDiscoveryDiagnostic {
109    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
110        match self {
111            Self::MissingLakeRoot { requested_root } => {
112                write!(
113                    f,
114                    "lean-toolchain: no Lake project found at {} or {}/lean",
115                    requested_root.display(),
116                    requested_root.display()
117                )
118            }
119            Self::MissingModuleRoot {
120                project_root,
121                module_root,
122            } => {
123                write!(
124                    f,
125                    "lean-toolchain: module root `{module_root}` was not found in {}",
126                    project_root.display()
127                )
128            }
129            Self::InvalidModuleName { module, reason } => {
130                write!(f, "lean-toolchain: invalid Lean module name `{module}`: {reason}")
131            }
132            Self::UnsupportedToolchain {
133                active,
134                supported_window,
135            } => {
136                write!(
137                    f,
138                    "lean-toolchain: active Lean toolchain {active} is not in the supported window: {supported_window}"
139                )
140            }
141            Self::Io { path, message, source } => {
142                write!(f, "lean-toolchain: {message} at {}: {source}", path.display())
143            }
144        }
145    }
146}
147
148impl std::error::Error for LeanModuleDiscoveryDiagnostic {
149    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
150        match self {
151            Self::Io { source, .. } => Some(source),
152            Self::MissingLakeRoot { .. }
153            | Self::MissingModuleRoot { .. }
154            | Self::InvalidModuleName { .. }
155            | Self::UnsupportedToolchain { .. } => None,
156        }
157    }
158}
159
160/// Discover Lean modules in a Lake project.
161///
162/// # Errors
163///
164/// Returns typed diagnostics when the Lake root cannot be found, the active
165/// toolchain is unsupported, a selected module root is missing, a module name
166/// cannot be represented safely, or source traversal fails.
167pub fn discover_lake_modules(
168    options: LeanModuleDiscoveryOptions,
169) -> Result<LeanLakeProjectModules, LeanModuleDiscoveryDiagnostic> {
170    if !options.toolchain.is_supported() {
171        return Err(LeanModuleDiscoveryDiagnostic::UnsupportedToolchain {
172            active: options.toolchain.lean_version.to_owned(),
173            supported_window: supported_window(),
174        });
175    }
176
177    let requested_root = normalize_existing(&options.requested_root)?;
178    let (project_root, lakefile) = lake_root_for(&requested_root)?;
179    let module_roots = discover_module_roots(&project_root, &lakefile)?;
180    let selected_roots = options.selected_roots.unwrap_or_else(|| module_roots.clone());
181    for root in &selected_roots {
182        validate_module_name(root)?;
183        if !module_root_exists(&project_root, root) {
184            return Err(LeanModuleDiscoveryDiagnostic::MissingModuleRoot {
185                project_root,
186                module_root: root.clone(),
187            });
188        }
189    }
190
191    let modules = enumerate_sources(&project_root, &selected_roots)?;
192    let fingerprint = fingerprint_source_set(&project_root, &lakefile, &modules, options.toolchain)?;
193    Ok(LeanLakeProjectModules {
194        requested_root,
195        project_root,
196        lakefile,
197        module_roots,
198        selected_roots,
199        modules,
200        fingerprint,
201    })
202}
203
204/// Return whether a Lake `lean_lib` target is declared in a project.
205///
206/// # Errors
207///
208/// Returns discovery diagnostics if the Lake root or lakefile cannot be read.
209pub fn lake_target_declared(project_root: &Path, target_name: &str) -> Result<bool, LeanModuleDiscoveryDiagnostic> {
210    let requested_root = normalize_existing(project_root)?;
211    let (_project_root, lakefile) = lake_root_for(&requested_root)?;
212    let contents = read_to_string(&lakefile, "could not read Lake file")?;
213    let quoted = format!("lean_lib «{target_name}»");
214    let bare = format!("lean_lib {target_name}");
215    let string = format!("lean_lib \"{target_name}\"");
216    Ok(contents.contains(&quoted) || contents.contains(&bare) || contents.contains(&string))
217}
218
219fn normalize_existing(path: &Path) -> Result<PathBuf, LeanModuleDiscoveryDiagnostic> {
220    let expanded = expand_home(path);
221    if !expanded.exists() {
222        return Err(LeanModuleDiscoveryDiagnostic::MissingLakeRoot {
223            requested_root: expanded,
224        });
225    }
226    fs::canonicalize(&expanded).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
227        path: expanded,
228        message: "could not canonicalize path",
229        source,
230    })
231}
232
233fn expand_home(path: &Path) -> PathBuf {
234    let Some(text) = path.to_str() else {
235        return path.to_path_buf();
236    };
237    if text == "~" {
238        return home_dir().unwrap_or_else(|| path.to_path_buf());
239    }
240    if let Some(rest) = text.strip_prefix("~/")
241        && let Some(home) = home_dir()
242    {
243        return home.join(rest);
244    }
245    path.to_path_buf()
246}
247
248fn home_dir() -> Option<PathBuf> {
249    std::env::var_os("HOME").map(PathBuf::from)
250}
251
252fn lake_root_for(path: &Path) -> Result<(PathBuf, PathBuf), LeanModuleDiscoveryDiagnostic> {
253    if let Some(lakefile) = lakefile_path(path) {
254        return Ok((path.to_path_buf(), lakefile));
255    }
256    let nested = path.join("lean");
257    if let Some(lakefile) = lakefile_path(&nested) {
258        return Ok((nested, lakefile));
259    }
260    Err(LeanModuleDiscoveryDiagnostic::MissingLakeRoot {
261        requested_root: path.to_path_buf(),
262    })
263}
264
265fn lakefile_path(root: &Path) -> Option<PathBuf> {
266    let toml = root.join("lakefile.toml");
267    if toml.is_file() {
268        return Some(toml);
269    }
270    let lean = root.join("lakefile.lean");
271    lean.is_file().then_some(lean)
272}
273
274fn discover_module_roots(project_root: &Path, lakefile: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
275    let mut roots = if lakefile.file_name().and_then(|name| name.to_str()) == Some("lakefile.toml") {
276        discover_toml_lakefile_roots(lakefile)?
277    } else {
278        discover_lean_lakefile_roots(lakefile)?
279    };
280    if roots.is_empty() {
281        roots = discover_top_level_roots(project_root)?;
282    }
283    roots.sort();
284    roots.dedup();
285    for root in &roots {
286        validate_module_name(root)?;
287    }
288    Ok(roots)
289}
290
291fn discover_toml_lakefile_roots(lakefile: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
292    let text = read_to_string(lakefile, "could not read Lake TOML file")?;
293    let mut roots = Vec::new();
294    let mut in_lean_lib = false;
295    for line in text.lines() {
296        let trimmed = line.trim();
297        if trimmed == "[[lean_lib]]" {
298            in_lean_lib = true;
299            continue;
300        }
301        if trimmed.starts_with("[[") || trimmed.starts_with('[') {
302            in_lean_lib = false;
303            continue;
304        }
305        if in_lean_lib
306            && let Some(raw) = trimmed.strip_prefix("name")
307            && let Some((_eq, value)) = raw.split_once('=')
308        {
309            let root = normalize_lake_identifier(value);
310            if !root.is_empty() {
311                roots.push(root);
312            }
313        }
314    }
315    Ok(roots)
316}
317
318fn discover_lean_lakefile_roots(lakefile: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
319    let text = read_to_string(lakefile, "could not read Lake file")?;
320    Ok(text
321        .lines()
322        .filter_map(|line| {
323            let trimmed = line.trim_start();
324            let rest = trimmed.strip_prefix("lean_lib ")?;
325            let raw = rest.split_whitespace().next()?;
326            let root = normalize_lake_identifier(raw);
327            (!root.is_empty()).then_some(root)
328        })
329        .collect())
330}
331
332fn discover_top_level_roots(project_root: &Path) -> Result<Vec<String>, LeanModuleDiscoveryDiagnostic> {
333    let mut roots = Vec::new();
334    for entry in fs::read_dir(project_root).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
335        path: project_root.to_path_buf(),
336        message: "could not read Lake project directory",
337        source,
338    })? {
339        let entry = entry.map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
340            path: project_root.to_path_buf(),
341            message: "could not read Lake project directory entry",
342            source,
343        })?;
344        let path = entry.path();
345        if path.extension().and_then(|extension| extension.to_str()) == Some("lean")
346            && let Some(stem) = path.file_stem().and_then(|stem| stem.to_str())
347        {
348            roots.push(stem.to_owned());
349        }
350    }
351    Ok(roots)
352}
353
354fn module_root_exists(project_root: &Path, module_root: &str) -> bool {
355    module_to_file(project_root, module_root).is_file() || module_to_dir(project_root, module_root).is_dir()
356}
357
358fn enumerate_sources(
359    project_root: &Path,
360    selected_roots: &[String],
361) -> Result<Vec<LeanModuleDescriptor>, LeanModuleDiscoveryDiagnostic> {
362    let mut modules = std::collections::BTreeMap::<String, LeanModuleDescriptor>::new();
363    for source_root in selected_roots {
364        let root_file = module_to_file(project_root, source_root);
365        if root_file.is_file() {
366            modules.insert(
367                source_root.clone(),
368                LeanModuleDescriptor {
369                    module: source_root.clone(),
370                    path: root_file,
371                    source_root: source_root.clone(),
372                },
373            );
374        }
375
376        let module_dir = module_to_dir(project_root, source_root);
377        if module_dir.is_dir() {
378            collect_sources(project_root, &module_dir, source_root, &mut modules)?;
379        }
380    }
381    Ok(modules.into_values().collect())
382}
383
384fn collect_sources(
385    project_root: &Path,
386    dir: &Path,
387    source_root: &str,
388    modules: &mut std::collections::BTreeMap<String, LeanModuleDescriptor>,
389) -> Result<(), LeanModuleDiscoveryDiagnostic> {
390    for entry in fs::read_dir(dir).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
391        path: dir.to_path_buf(),
392        message: "could not read Lean source directory",
393        source,
394    })? {
395        let entry = entry.map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
396            path: dir.to_path_buf(),
397            message: "could not read Lean source directory entry",
398            source,
399        })?;
400        let path = entry.path();
401        let metadata = entry.metadata().map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
402            path: path.clone(),
403            message: "could not stat Lean source path",
404            source,
405        })?;
406        if metadata.is_dir() {
407            collect_sources(project_root, &path, source_root, modules)?;
408        } else if path.extension().and_then(|extension| extension.to_str()) == Some("lean") {
409            let module = module_from_path(project_root, &path)?;
410            validate_module_name(&module)?;
411            modules.insert(
412                module.clone(),
413                LeanModuleDescriptor {
414                    module,
415                    path,
416                    source_root: source_root.to_owned(),
417                },
418            );
419        }
420    }
421    Ok(())
422}
423
424fn fingerprint_source_set(
425    project_root: &Path,
426    lakefile: &Path,
427    modules: &[LeanModuleDescriptor],
428    toolchain: ToolchainFingerprint,
429) -> Result<LeanModuleSetFingerprint, LeanModuleDiscoveryDiagnostic> {
430    let lakefile_sha256 = sha256_file(lakefile)?;
431    let manifest = project_root.join("lake-manifest.json");
432    let manifest_sha256 = if manifest.is_file() {
433        Some(sha256_file(&manifest)?)
434    } else {
435        None
436    };
437    let mut source_max_mtime_ns = 0_u128;
438    for module in modules {
439        let metadata = fs::metadata(&module.path).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
440            path: module.path.clone(),
441            message: "could not stat Lean module source",
442            source,
443        })?;
444        let modified = metadata
445            .modified()
446            .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
447                path: module.path.clone(),
448                message: "could not read Lean module source mtime",
449                source,
450            })?;
451        let mtime_ns = modified
452            .duration_since(UNIX_EPOCH)
453            .map_or(0, |duration| duration.as_nanos());
454        source_max_mtime_ns = source_max_mtime_ns.max(mtime_ns);
455    }
456    Ok(LeanModuleSetFingerprint {
457        toolchain,
458        lakefile_sha256,
459        manifest_sha256,
460        source_count: modules.len() as u64,
461        source_max_mtime_ns,
462    })
463}
464
465fn sha256_file(path: &Path) -> Result<String, LeanModuleDiscoveryDiagnostic> {
466    fs::read(path)
467        .map(|bytes| sha256_hex(&bytes))
468        .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
469            path: path.to_path_buf(),
470            message: "could not read file for fingerprinting",
471            source,
472        })
473}
474
475fn sha256_hex(bytes: &[u8]) -> String {
476    let mut hasher = Sha256::new();
477    hasher.update(bytes);
478    let digest = hasher.finalize();
479    let mut out = String::with_capacity(digest.len().saturating_mul(2));
480    for byte in digest {
481        use std::fmt::Write as _;
482        if write!(out, "{byte:02x}").is_err() {
483            return out;
484        }
485    }
486    out
487}
488
489fn module_from_path(project_root: &Path, path: &Path) -> Result<String, LeanModuleDiscoveryDiagnostic> {
490    let relative = path
491        .strip_prefix(project_root)
492        .map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
493            path: path.to_path_buf(),
494            message: "could not relativize Lean source path",
495            source: std::io::Error::other(source),
496        })?;
497    let mut parts: Vec<String> = relative
498        .components()
499        .map(|component| component.as_os_str().to_string_lossy().into_owned())
500        .collect();
501    if let Some(last) = parts.last_mut()
502        && let Some(stripped) = last.strip_suffix(".lean")
503    {
504        *last = stripped.to_owned();
505    }
506    Ok(parts.join("."))
507}
508
509fn module_to_file(project_root: &Path, module: &str) -> PathBuf {
510    let mut path = module_to_dir(project_root, module);
511    path.set_extension("lean");
512    path
513}
514
515fn module_to_dir(project_root: &Path, module: &str) -> PathBuf {
516    let mut path = project_root.to_path_buf();
517    for part in module.split('.') {
518        path.push(part);
519    }
520    path
521}
522
523fn normalize_lake_identifier(raw: &str) -> String {
524    raw.trim()
525        .trim_matches('`')
526        .trim_matches('«')
527        .trim_matches('»')
528        .trim_matches('"')
529        .trim()
530        .to_owned()
531}
532
533fn validate_module_name(module: &str) -> Result<(), LeanModuleDiscoveryDiagnostic> {
534    if module.is_empty() {
535        return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
536            module: module.to_owned(),
537            reason: "module name is empty".to_owned(),
538        });
539    }
540    for component in module.split('.') {
541        if component.is_empty() {
542            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
543                module: module.to_owned(),
544                reason: "module name contains an empty component".to_owned(),
545            });
546        }
547        let mut chars = component.chars();
548        let Some(first) = chars.next() else {
549            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
550                module: module.to_owned(),
551                reason: "module name contains an empty component".to_owned(),
552            });
553        };
554        if !(first == '_' || first.is_alphabetic()) {
555            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
556                module: module.to_owned(),
557                reason: "module components must begin with a letter or underscore".to_owned(),
558            });
559        }
560        if chars.any(|ch| !(ch == '_' || ch == '\'' || ch.is_alphanumeric())) {
561            return Err(LeanModuleDiscoveryDiagnostic::InvalidModuleName {
562                module: module.to_owned(),
563                reason: "module components may contain only letters, digits, underscores, or apostrophes".to_owned(),
564            });
565        }
566    }
567    Ok(())
568}
569
570fn read_to_string(path: &Path, message: &'static str) -> Result<String, LeanModuleDiscoveryDiagnostic> {
571    fs::read_to_string(path).map_err(|source| LeanModuleDiscoveryDiagnostic::Io {
572        path: path.to_path_buf(),
573        message,
574        source,
575    })
576}
577
578fn supported_window() -> String {
579    lean_rs_sys::SUPPORTED_TOOLCHAINS
580        .iter()
581        .map(|entry| format!("{:?}", entry.versions))
582        .collect::<Vec<_>>()
583        .join(", ")
584}
585
586#[cfg(test)]
587#[allow(
588    clippy::expect_used,
589    clippy::panic,
590    clippy::unwrap_used,
591    clippy::wildcard_enum_match_arm
592)]
593mod tests {
594    use super::{
595        LeanModuleDiscoveryDiagnostic, LeanModuleDiscoveryOptions, discover_lake_modules, lake_target_declared,
596    };
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 target_declaration_probe_is_typed() {
689        let root = temp_project("target-probe");
690        write_file(
691            &root.join("lakefile.lean"),
692            "package demo\nlean_lib Demo where\nlean_lib Extra where\n",
693        );
694        assert!(lake_target_declared(&root, "Demo").unwrap());
695        assert!(!lake_target_declared(&root, "Missing").unwrap());
696    }
697
698    fn module_names(project: &super::LeanLakeProjectModules) -> Vec<&str> {
699        project.modules.iter().map(|module| module.module.as_str()).collect()
700    }
701
702    fn temp_project(name: &str) -> PathBuf {
703        let root = std::env::temp_dir().join(format!("lean-toolchain-modules-{name}-{}", std::process::id()));
704        if root.exists() {
705            fs::remove_dir_all(&root).unwrap();
706        }
707        fs::create_dir_all(&root).unwrap();
708        root
709    }
710
711    fn write_file(path: &Path, contents: &str) {
712        if let Some(parent) = path.parent() {
713            fs::create_dir_all(parent).unwrap();
714        }
715        fs::write(path, contents).unwrap();
716    }
717}
lean_toolchain/modules.rs

lean_toolchain/
modules.rs
