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