lean_toolchain/diagnostics.rs
1//! Layered link-time / discovery diagnostics.
2//!
3//! Each variant `Display`s as exactly one line so the message can be emitted
4//! verbatim via `cargo:warning=`.
5
6use std::fmt;
7use std::path::PathBuf;
8
9/// Reasons the Lean toolchain or its linkage could not be resolved.
10///
11/// Variants carry enough context to produce a single actionable diagnostic.
12/// The enum is `#[non_exhaustive]` — adding a new failure mode is not a
13/// breaking change.
14#[non_exhaustive]
15#[derive(Debug)]
16pub enum LinkDiagnostics {
17 /// No discovery probe could locate a Lean prefix containing `include/lean/lean.h`.
18 MissingLean {
19 /// One human-readable line per probe attempted, in precedence order.
20 tried: Vec<String>,
21 },
22 /// A discovered prefix is missing the expected header file.
23 MissingHeader {
24 /// Where the header was expected to live.
25 path: PathBuf,
26 },
27 /// A required Lean library was not found in any search directory.
28 MissingLib {
29 /// Library name as it would appear in `-l<name>`.
30 name: String,
31 /// Directories searched, in order.
32 search_dirs: Vec<PathBuf>,
33 },
34 /// The discovered Lean version disagrees with the build-baked one.
35 VersionMismatch {
36 /// Version this build of `lean-toolchain` was compiled against.
37 expected: String,
38 /// Version reported by the active toolchain at runtime.
39 actual: String,
40 },
41 /// A symbol in the required-symbols allowlist failed to resolve.
42 AllowlistFailure {
43 /// Name of the missing symbol.
44 name: &'static str,
45 },
46 /// A built Lake fixture artifact is missing.
47 FixtureArtifactMissing {
48 /// Path to the missing artifact.
49 path: PathBuf,
50 /// One-liner recovery command for the embedder.
51 recovery: &'static str,
52 },
53 /// The active Lean toolchain is outside the supported window
54 /// declared by [`lean_rs_sys::SUPPORTED_TOOLCHAINS`].
55 UnsupportedToolchain {
56 /// `LEAN_VERSION_STRING` of the active toolchain.
57 active: String,
58 /// Comma-joined `versions` arrays from each
59 /// [`SupportedToolchain`](lean_rs_sys::SupportedToolchain) entry,
60 /// rendered as `["4.23.0", "4.24.0", "4.24.1"], ["4.25.0", ...], ...`.
61 supported_window: String,
62 },
63 /// The requested Lake target was not declared in the project's lakefile.
64 LakeTargetMissing {
65 /// Directory expected to contain the project's lakefile.
66 project_root: PathBuf,
67 /// Requested Lake target name.
68 target_name: String,
69 },
70 /// The `lake` executable could not be started.
71 LakeUnavailable {
72 /// Directory where the Lake command would have run.
73 project_root: PathBuf,
74 /// Requested Lake target name.
75 target_name: String,
76 /// One-line process-spawn failure.
77 detail: String,
78 },
79 /// `lake build <target>:shared` exited unsuccessfully.
80 LakeBuildFailed {
81 /// Directory where the Lake command ran.
82 project_root: PathBuf,
83 /// Requested Lake target name.
84 target_name: String,
85 /// Process exit status rendered for diagnostics.
86 status: String,
87 /// Bounded one-line stdout/stderr summary from Lake.
88 detail: String,
89 },
90 /// Lake completed, but `lean-toolchain` could not resolve the expected dylib path.
91 LakeOutputUnresolved {
92 /// Directory expected to contain the Lake project.
93 project_root: PathBuf,
94 /// Requested Lake target name.
95 target_name: String,
96 /// One-line reason, including the path or manifest field that was missing.
97 reason: String,
98 },
99}
100
101impl fmt::Display for LinkDiagnostics {
102 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
103 match self {
104 Self::MissingLean { tried } => {
105 // Keep the message on one line: collapse the per-probe records
106 // with a literal "; ".
107 let joined = tried.join("; ");
108 write!(f, "lean-toolchain: no Lean toolchain found; tried: {joined}")
109 }
110 Self::MissingHeader { path } => {
111 write!(f, "lean-toolchain: missing Lean header at {}", path.display())
112 }
113 Self::MissingLib { name, search_dirs } => {
114 let dirs = search_dirs
115 .iter()
116 .map(|p| p.display().to_string())
117 .collect::<Vec<_>>()
118 .join(":");
119 write!(f, "lean-toolchain: missing Lean library `{name}` (searched: {dirs})")
120 }
121 Self::VersionMismatch { expected, actual } => {
122 write!(
123 f,
124 "lean-toolchain: Lean version mismatch: built against {expected}, discovered {actual}"
125 )
126 }
127 Self::AllowlistFailure { name } => {
128 write!(f, "lean-toolchain: required symbol `{name}` failed to resolve")
129 }
130 Self::FixtureArtifactMissing { path, recovery } => {
131 write!(
132 f,
133 "lean-toolchain: missing fixture artifact {} (recovery: {recovery})",
134 path.display()
135 )
136 }
137 Self::UnsupportedToolchain {
138 active,
139 supported_window,
140 } => {
141 write!(
142 f,
143 "lean-toolchain: active Lean toolchain {active} is not in the supported window: {supported_window}"
144 )
145 }
146 Self::LakeTargetMissing {
147 project_root,
148 target_name,
149 } => {
150 write!(
151 f,
152 "lean-toolchain: Lake target `{target_name}` is not declared in {}",
153 project_root.display()
154 )
155 }
156 Self::LakeUnavailable {
157 project_root,
158 target_name,
159 detail,
160 } => {
161 write!(
162 f,
163 "lean-toolchain: could not start `lake build {target_name}:shared` in {}: {detail}",
164 project_root.display()
165 )
166 }
167 Self::LakeBuildFailed {
168 project_root,
169 target_name,
170 status,
171 detail,
172 } => {
173 write!(
174 f,
175 "lean-toolchain: `lake build {target_name}:shared` failed in {} with {status}: {detail}",
176 project_root.display()
177 )
178 }
179 Self::LakeOutputUnresolved {
180 project_root,
181 target_name,
182 reason,
183 } => {
184 write!(
185 f,
186 "lean-toolchain: could not resolve Lake output for target `{target_name}` in {}: {reason}",
187 project_root.display()
188 )
189 }
190 }
191 }
192}
193
194impl std::error::Error for LinkDiagnostics {}