Enum Error 

pub enum Error {
    NonUtf8Path {
        path: PathBuf,
    },
    PathDoesNotExist {
        path: Utf8PathBuf,
    },
    NotLeanFile {
        path: Utf8PathBuf,
    },
    InvalidLineSpec {
        spec: String,
    },
    Io(Error),
    Json(Error),
    ConfigRead {
        path: Utf8PathBuf,
        source: Error,
    },
    ConfigParse {
        path: Utf8PathBuf,
        source: Error,
    },
    Timeout {
        file: Utf8PathBuf,
        timeout_seconds: u64,
    },
    OutsideWorkspace {
        path: Utf8PathBuf,
    },
    ZeroLineSpan {
        file: Utf8PathBuf,
    },
    InvertedSpan {
        file: Utf8PathBuf,
        start_line: u32,
        end_line: u32,
    },
    SpanOutOfBounds {
        file: Utf8PathBuf,
        start_line: u32,
        end_line: u32,
        line_count: usize,
    },
    MultiFileEditNotAllowed {
        files: usize,
    },
    DisallowedReplacement {
        file: Utf8PathBuf,
        detail: String,
    },
    RunnerSpawn {
        runner: Utf8PathBuf,
        source: Error,
    },
    RunnerProtocol {
        detail: String,
    },
    WorkspaceCopy {
        path: Utf8PathBuf,
        source: Error,
    },
    Todo {
        feature: &'static str,
    },
}

Errors produced by tracing, parsing, discovery, and writing.

Variants

NonUtf8Path

A filesystem path could not be represented as UTF-8.

Fields

path: PathBuf

Original path rendered lossily.

PathDoesNotExist

A requested path does not exist.

Fields

path: Utf8PathBuf

Missing path.

NotLeanFile

A requested path is not a Lean source file.

Fields

path: Utf8PathBuf

Invalid file path.

InvalidLineSpec

A FILE.lean:LINE target could not be parsed.

Fields

spec: String

The raw target string as given.

Io(Error)

IO failure.

Json(Error)

JSON serialization/deserialization failure.

ConfigRead

A config file could not be read from disk.

Fields

path: Utf8PathBuf

Config file path.

source: Error

Underlying IO error.

ConfigParse

A config file could not be parsed as TOML.

Fields

path: Utf8PathBuf

Config file path.

source: Error

Underlying TOML parse error.

Timeout

External Lean/Lake process timed out.

Fields

file: Utf8PathBuf

File being checked.

timeout_seconds: u64

Timeout in seconds.

OutsideWorkspace

An edit path is absolute or uses .., so it could escape the workspace.

Fields

path: Utf8PathBuf

The offending relative path as given.

ZeroLineSpan

A span carried a zero line number; lines are one-based.

Fields

file: Utf8PathBuf

File the span pointed at.

InvertedSpan

A span’s start line is greater than its end line.

Fields

file: Utf8PathBuf

File the span pointed at.

start_line: u32

One-based first line.

end_line: u32

One-based last line.

SpanOutOfBounds

A span falls outside the target file’s line range.

Fields

file: Utf8PathBuf

File the span pointed at.

start_line: u32

One-based first line.

end_line: u32

One-based last line.

line_count: usize

Number of lines actually present.

MultiFileEditNotAllowed

An attempt edits more than one file without the multi-file flag.

Fields

files: usize

Distinct files the attempt touched.

DisallowedReplacement

A replacement would splice a top-level command into the edited file.

A single-span patch is a proof body; a column-zero command such as #eval/#print/import/set_option/macro/elab/open is refused so it cannot perturb the accept guards that read the compile.

Fields

file: Utf8PathBuf

File the span pointed at.

detail: String

The offending line and why it was refused.

RunnerSpawn

Starting the external agent runner failed.

Fields

runner: Utf8PathBuf

Runner path that could not be started.

source: Error

Underlying IO error.

RunnerProtocol

The runner broke the line-oriented request/response contract.

Fields

detail: String

What went wrong with the runner exchange.

WorkspaceCopy

Copying the Lake project into an isolated workspace failed.

Fields

path: Utf8PathBuf

Path being copied when the failure happened.

source: Error

Underlying IO error.

Todo

Placeholder for code paths intentionally left as TODO.

Fields

feature: &'static str

Feature name.

Trait Implementations

impl Debug for Error

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Error

fn fmt(&self, __formatter: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Error for Error

fn source(&self) -> Option<&(dyn Error + 'static)>

Returns the lower-level source of this error, if any.

fn description(&self) -> &str

👎Deprecated since 1.42.0:

use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎Deprecated since 1.33.0:

replaced by Error::source, which can support downcasting

fn provide<'a>(&'a self, request: &mut Request<'a>)

🔬This is a nightly-only experimental API. (error_generic_member_access)

Provides type-based access to context intended for error reports.

impl From<Error> for Error

fn from(source: Error) -> Self

Converts to this type from the input type.

impl From<Error> for Error

fn from(source: Error) -> Self

Converts to this type from the input type.