Unify pyAnalyzeLaurel error classification#1131
Conversation
The two pipeline stages (Python→Laurel, Laurel→Core) each had their own error-handling block, and the Laurel→Core one misreported user-facing errors as internal. Now both stages throw List DiagnosticModel and route through a single classifier that maps DiagnosticType to exit category. Preserves existing user_errors.txt and DETAIL formatting.
|
@tautschnig Then I can use that to solve your suggestions in PR #1118 |
Satisfies lake lint's requirement that every Strata module be transitively imported from the library root.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🔍 Clean unification — the single classifier approach is a good simplification and the new test demonstrates the Laurel→Core user-error path that was previously misreported. A few items below.
| /-- Errors from the pyAnalyzeLaurel pipeline: a batch of diagnostics. | ||
|
|
||
| Each entry carries a `DiagnosticType` (UserError, NotYetImplemented, StrataBug, | ||
| or Warning) so the caller can classify the batch into a single exit category |
There was a problem hiding this comment.
🔍 This docstring references "the prior three-case PipelineError inductive" — comments should be stateless and not reference previous versions of the code. Consider rephrasing to describe what this type is without referencing what it replaced.
|
|
||
| /-- Helper: create a known-limitation diagnostic (intentionally unsupported). -/ | ||
| public def mkKnownLimitationDiagnostic (msg : String) : DiagnosticModel := | ||
| { fileRange := FileRange.unknown, message := msg, type := .NotYetImplemented } |
There was a problem hiding this comment.
🔍 mkKnownLimitationDiagnostic and mkInternalDiagnostic duplicate DiagnosticModel.fromMessage (defined in FileRange.lean) — they're equivalent to DiagnosticModel.fromMessage msg (type := .NotYetImplemented) and DiagnosticModel.fromMessage msg (type := .StrataBug) respectively. mkUserCodeDiagnostic adds the file/range so it has a reason to exist, but the other two could be inlined or replaced by the existing helper.
|
|
||
| /-- Classify diagnostics and exit with the matching `pyAnalyzeLaurel` category. | ||
| `prefixMsg` is prepended to internal-error and known-limitation details; | ||
| user-error details use the diagnostic's own message + line/column only. -/ |
There was a problem hiding this comment.
🔍 Docstring says "prefixMsg is prepended to internal-error and known-limitation details" but it's only used in the internalError branch. The knownLimitation branch uses d.message directly.
| match userDiags.head? with | ||
| | none => pure () | ||
| | some d => | ||
| let filePath := match d.fileRange.file with | .file p => p |
There was a problem hiding this comment.
🔍 let filePath := match d.fileRange.file with | .file p => p — this is fine today since Uri has a single constructor, but if Uri ever gains another case (e.g., a URI scheme), this will silently break. A destructuring let .file filePath := d.fileRange.file would make the intent clearer and produce a compile error if Uri grows.
julesmt
force-pushed
the
julesmt/feature/unify-pipeline-diagnostics
branch
from
d7f41b0 to
88245df
Compare
- PySpecPipeline: trim PipelineError/mkUserCodeDiagnostic docstrings; drop mkKnownLimitationDiagnostic / mkInternalDiagnostic (duplicated DiagnosticModel.fromMessage) and inline call sites via a local internalErr closure. - StrataMain: tighten classifyDiagnosticsAndExit docstring (prefixMsg only prefixes internal-error details), fold the two duplicate filter/head? blocks into a firstOf helper, flatten emitUserErrorsFile with an early-return and destructuring `let .file filePath := …` so a future Uri case fails to compile.
|
@MikaelMayer thanks for your review. I tried to apply your suggestions :). |
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🔍 LGTM — all comments addressed.
|
@tautschnig could you be my second reviewer for merge, like that I can rewrite the other PR this afternoon |
|
This conflicts with #1093. I think unifying the concepts is good, but Laurel to core failures should be treated as internal errors. We should stop generating invalid laurel rather than rely on it to catch bugs. |
3 participants
The two pipeline stages (Python→Laurel, Laurel→Core) each had their own error-handling block, and the Laurel→Core one misreported user-facing errors as internal. Now both stages throw List DiagnosticModel and route through a single classifier that maps DiagnosticType to exit category. Preserves existing user_errors.txt and DETAIL formatting.
Issue #, if available:
Description of changes:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.