lean-agent-core 0.2.0

Core library for tracing Lean 4 diagnostics and evaluating Lean theorem-proving agents.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

//! Lean file discovery.

use crate::{Error, LeanFile, Result};
use camino::{Utf8Path, Utf8PathBuf};
use ignore::WalkBuilder;

/// Discover Lean source files from a file or directory.
pub fn discover_lean_files(path: &Utf8Path, recursive: bool) -> Result<Vec<LeanFile>> {
    if !path.exists() {
        return Err(Error::PathDoesNotExist {
            path: path.to_path_buf(),
        });
    }

    if path.is_file() {
        return Ok(vec![LeanFile::new(path.to_path_buf())?]);
    }

    let mut files = Vec::new();
    let mut builder = WalkBuilder::new(path);
    builder
        .hidden(false)
        .parents(true)
        .git_ignore(true)
        .git_exclude(true);

    if !recursive {
        builder.max_depth(Some(1));
    }

    for entry in builder.build() {
        let entry = entry.map_err(|err| Error::Io(std::io::Error::other(err)))?;
        if !entry
            .file_type()
            .is_some_and(|file_type| file_type.is_file())
        {
            continue;
        }
        let std_path = entry.into_path();
        let utf8 = Utf8PathBuf::from_path_buf(std_path.clone())
            .map_err(|_| Error::NonUtf8Path { path: std_path })?;
        if utf8.extension() == Some("lean") {
            files.push(LeanFile::new(utf8)?);
        }
    }

    files.sort();
    Ok(files)
}