lean_agent_core/
error.rs

1//! Error types for `lean-agent-core`.
2
3use camino::Utf8PathBuf;
4use thiserror::Error;
5
6/// Project-local result alias.
7pub type Result<T> = std::result::Result<T, Error>;
8
9/// Errors produced by tracing, parsing, discovery, and writing.
10#[derive(Debug, Error)]
11pub enum Error {
12    /// A filesystem path could not be represented as UTF-8.
13    #[error("path is not valid UTF-8: {path:?}")]
14    NonUtf8Path {
15        /// Original path rendered lossily.
16        path: std::path::PathBuf,
17    },
18
19    /// A requested path does not exist.
20    #[error("path does not exist: {path}")]
21    PathDoesNotExist {
22        /// Missing path.
23        path: Utf8PathBuf,
24    },
25
26    /// A requested path is not a Lean source file.
27    #[error("not a .lean file: {path}")]
28    NotLeanFile {
29        /// Invalid file path.
30        path: Utf8PathBuf,
31    },
32
33    /// A `FILE.lean:LINE` target could not be parsed.
34    #[error("invalid FILE.lean:LINE target: {spec}")]
35    InvalidLineSpec {
36        /// The raw target string as given.
37        spec: String,
38    },
39
40    /// IO failure.
41    #[error(transparent)]
42    Io(#[from] std::io::Error),
43
44    /// JSON serialization/deserialization failure.
45    #[error(transparent)]
46    Json(#[from] serde_json::Error),
47
48    /// A config file could not be read from disk.
49    #[error("reading config {path}: {source}")]
50    ConfigRead {
51        /// Config file path.
52        path: Utf8PathBuf,
53        /// Underlying IO error.
54        #[source]
55        source: std::io::Error,
56    },
57
58    /// A config file could not be parsed as TOML.
59    #[error("parsing config {path}: {source}")]
60    ConfigParse {
61        /// Config file path.
62        path: Utf8PathBuf,
63        /// Underlying TOML parse error.
64        #[source]
65        source: toml::de::Error,
66    },
67
68    /// External Lean/Lake process timed out.
69    #[error("Lean process timed out after {timeout_seconds}s for {file}")]
70    Timeout {
71        /// File being checked.
72        file: Utf8PathBuf,
73        /// Timeout in seconds.
74        timeout_seconds: u64,
75    },
76
77    /// An edit path is absolute or uses `..`, so it could escape the workspace.
78    #[error("edit path escapes the workspace root: {path}")]
79    OutsideWorkspace {
80        /// The offending relative path as given.
81        path: Utf8PathBuf,
82    },
83
84    /// A span carried a zero line number; lines are one-based.
85    #[error("span line numbers must be one-based and non-zero (file {file})")]
86    ZeroLineSpan {
87        /// File the span pointed at.
88        file: Utf8PathBuf,
89    },
90
91    /// A span's start line is greater than its end line.
92    #[error("inverted span in {file}: start_line {start_line} > end_line {end_line}")]
93    InvertedSpan {
94        /// File the span pointed at.
95        file: Utf8PathBuf,
96        /// One-based first line.
97        start_line: u32,
98        /// One-based last line.
99        end_line: u32,
100    },
101
102    /// A span falls outside the target file's line range.
103    #[error("span {start_line}..={end_line} is outside {file} ({line_count} lines)")]
104    SpanOutOfBounds {
105        /// File the span pointed at.
106        file: Utf8PathBuf,
107        /// One-based first line.
108        start_line: u32,
109        /// One-based last line.
110        end_line: u32,
111        /// Number of lines actually present.
112        line_count: usize,
113    },
114
115    /// An attempt edits more than one file without the multi-file flag.
116    #[error("multi-file edit refused ({files} files); pass the multi-file flag to allow")]
117    MultiFileEditNotAllowed {
118        /// Distinct files the attempt touched.
119        files: usize,
120    },
121
122    /// A replacement would splice a top-level command into the edited file.
123    ///
124    /// A single-span patch is a proof body; a column-zero command such as
125    /// `#eval`/`#print`/`import`/`set_option`/`macro`/`elab`/`open` is refused so
126    /// it cannot perturb the accept guards that read the compile.
127    #[error("replacement in {file} introduces a top-level command: {detail}")]
128    DisallowedReplacement {
129        /// File the span pointed at.
130        file: Utf8PathBuf,
131        /// The offending line and why it was refused.
132        detail: String,
133    },
134
135    /// Starting the external agent runner failed.
136    #[error("failed to start runner {runner}: {source}")]
137    RunnerSpawn {
138        /// Runner path that could not be started.
139        runner: Utf8PathBuf,
140        /// Underlying IO error.
141        #[source]
142        source: std::io::Error,
143    },
144
145    /// The runner broke the line-oriented request/response contract.
146    #[error("runner protocol error: {detail}")]
147    RunnerProtocol {
148        /// What went wrong with the runner exchange.
149        detail: String,
150    },
151
152    /// Copying the Lake project into an isolated workspace failed.
153    #[error("workspace copy failed for {path}: {source}")]
154    WorkspaceCopy {
155        /// Path being copied when the failure happened.
156        path: Utf8PathBuf,
157        /// Underlying IO error.
158        #[source]
159        source: std::io::Error,
160    },
161
162    /// Placeholder for code paths intentionally left as TODO.
163    #[error("not implemented yet: {feature}")]
164    Todo {
165        /// Feature name.
166        feature: &'static str,
167    },
168}
lean_agent_core/error.rs

lean_agent_core/
error.rs
