From 856a87461b8464209235a7109dbee035a8aa09be Mon Sep 17 00:00:00 2001 From: Jules Date: Wed, 6 May 2026 11:35:49 -0700 Subject: [PATCH 1/3] Unify pyAnalyzeLaurel error classification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- Strata/Languages/Python/PySpecPipeline.lean | 57 +++++++----- Strata/Util/DiagnosticClassifier.lean | 36 ++++++++ StrataMain.lean | 91 ++++++++++++++----- .../test_laurel_to_core_user_error.expected | 6 ++ ...el_to_core_user_error.user_errors.expected | 4 + .../tests/test_laurel_to_core_user_error.py | 5 + StrataTest/Util/DiagnosticClassifier.lean | 31 +++++++ 7 files changed, 185 insertions(+), 45 deletions(-) create mode 100644 Strata/Util/DiagnosticClassifier.lean create mode 100644 StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected create mode 100644 StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected create mode 100644 StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py create mode 100644 StrataTest/Util/DiagnosticClassifier.lean diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index 21129ebe39..36a18815d8 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -390,20 +390,34 @@ public def translateCombinedLaurel (combined : Laurel.Program) let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined (profile := profile) return (coreOption, errors) -/-- Errors from the pyAnalyzeLaurel pipeline. -/ -public inductive PipelineError where - /-- The Python source contains invalid code (bad method name, wrong arguments, etc.). -/ - | userCode (range : SourceRange := .none) (msg : String) - /-- The pipeline encountered a Python construct it intentionally does not yet support. -/ - | knownLimitation (msg : String) - /-- An unexpected failure — likely a bug in the tool itself. -/ - | internal (msg : String) - -public instance : ToString PipelineError where - toString - | .userCode _ msg => s!"User code error: {msg}" - | .knownLimitation msg => s!"Known limitation: {msg}" - | .internal msg => msg +/-- 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 +using `classifyDiagnostics`. This type replaces the prior three-case +`PipelineError` inductive; routing is now driven by `DiagnosticType` rather +than by sum-type constructors, so the Python→Laurel and Laurel→Core pipeline +stages share a single classifier. -/ +public abbrev PipelineError := List DiagnosticModel + +/-- Helper: create a user-code error diagnostic. + +The optional `filePath`/`range` populate the `FileRange` used by +`classifyDiagnosticsAndExit` to format locations and by the +`user_errors.txt` side effect to emit SMT `set-info` lines. -/ +public def mkUserCodeDiagnostic (filePath : String) (range : SourceRange) (msg : String) + : DiagnosticModel := + { fileRange := { file := .file filePath, range := range } + message := msg + type := .UserError } + +/-- Helper: create a known-limitation diagnostic (intentionally unsupported). -/ +public def mkKnownLimitationDiagnostic (msg : String) : DiagnosticModel := + { fileRange := FileRange.unknown, message := msg, type := .NotYetImplemented } + +/-- Helper: create an internal-error diagnostic (tool bug). -/ +public def mkInternalDiagnostic (msg : String) : DiagnosticModel := + { fileRange := FileRange.unknown, message := msg, type := .StrataBug } /-- Run the pyAnalyzeLaurel pipeline: read a Python Ion program, resolve overloads from dispatch files, load PySpec declarations, @@ -430,15 +444,16 @@ public def pythonAndSpecToLaurel (quiet : Bool := false) (warningSummaryFile : Option String := none) : EIO PipelineError Laurel.Program := do + let metadataPath := sourcePath.getD pythonIonPath let stmts ← profileStep profile "Read Python Ion" do match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with | .ok r => pure r - | .error msg => throw (.internal msg) + | .error msg => throw [mkInternalDiagnostic msg] let result ← profileStep profile "Resolve and build Laurel prelude" do match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir (quiet := quiet) |>.toBaseIO with | .ok r => pure r - | .error msg => throw (.internal msg) + | .error msg => throw [mkInternalDiagnostic msg] -- Print and write PySpec warnings before later stages can fail let pyspecWarnings := result.pyspecWarnings @@ -468,19 +483,19 @@ public def pythonAndSpecToLaurel let preludeInfo := buildPreludeInfo result - let metadataPath := sourcePath.getD pythonIonPath let (laurelProgram, _ctx) ← profileStep profile "Translate Python to Laurel" do match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with - | .error (.userPythonError range msg) => throw (.userCode range msg) + | .error (.userPythonError range msg) => + throw [mkUserCodeDiagnostic metadataPath range msg] | .error (.unsupportedConstruct msg ast) => - throw (.knownLimitation s!"Unsupported construct: {msg}\nAST: {ast}") - | .error e => throw (.internal s!"Python to Laurel translation failed: {e}") + throw [mkKnownLimitationDiagnostic s!"Unsupported construct: {msg}\nAST: {ast}"] + | .error e => throw [mkInternalDiagnostic s!"Python to Laurel translation failed: {e}"] | .ok result => pure result let filteredPrelude ← profileStep profile "Filter prelude" do match Laurel.filterPrelude result.laurelProgram laurelProgram with | .ok prog => pure prog - | .error msg => throw (.internal msg) + | .error msg => throw [mkInternalDiagnostic msg] profileStep profile "Combine PySpec and user Laurel" do return combinePySpecLaurel filteredPrelude laurelProgram diff --git a/Strata/Util/DiagnosticClassifier.lean b/Strata/Util/DiagnosticClassifier.lean new file mode 100644 index 0000000000..a85ad507f1 --- /dev/null +++ b/Strata/Util/DiagnosticClassifier.lean @@ -0,0 +1,36 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Util.FileRange + +/-! # Diagnostic Classifier + +Priority order: StrataBug > UserError > NotYetImplemented. +Empty or warnings-only batches fall through to `internalError`. +-/ + +public section +namespace Strata + +inductive DiagnosticOutcome where + | internalError + | userError + | knownLimitation + deriving DecidableEq, Repr, Inhabited + +def classifyDiagnostics (diags : List DiagnosticModel) : DiagnosticOutcome := + if diags.any (fun d => d.type == DiagnosticType.StrataBug) then + .internalError + else if diags.any (fun d => d.type == DiagnosticType.UserError) then + .userError + else if diags.any (fun d => d.type == DiagnosticType.NotYetImplemented) then + .knownLimitation + else + .internalError + +end Strata +end diff --git a/StrataMain.lean b/StrataMain.lean index 179d04a6c0..9446e7e210 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -26,6 +26,7 @@ import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Languages.Laurel.Laurel import Strata.Languages.Core.EntryPoint import Strata.Transform.ProcedureInlining +import Strata.Util.DiagnosticClassifier import Strata.Util.IO import Strata.SimpleAPI @@ -506,6 +507,64 @@ private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do printPyAnalyzeResult "Known limitation" message IO.Process.exit ExitCode.knownLimitation +/-- Render diagnostics through `DiagnosticModel.format` so locations resolve + against the user's source. -/ +private def formatDiagnostics (diags : List DiagnosticModel) + (fileMap : Option Lean.FileMap) : String := + match fileMap with + | none => toString diags + | some _ => + String.intercalate "; " (diags.map (fun d => toString (d.format fileMap))) + +/-- Render a user-code diagnostic as "`msg` at line N, col M". -/ +private def formatUserErrorMessage (d : DiagnosticModel) (fileMap : Option Lean.FileMap) : String := + let location := if d.fileRange.range.isNone then "" else + match fileMap with + | some fm => + let pos := fm.toPosition d.fileRange.range.start + s!" at line {pos.line}, col {pos.column}" + | none => "" + s!"{d.message}{location}" + +/-- 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. -/ +private def classifyDiagnosticsAndExit {α} (prefixMsg : String) + (diags : List DiagnosticModel) (fileMap : Option Lean.FileMap) : IO α := do + match classifyDiagnostics diags with + | .internalError => + exitPyAnalyzeInternalError s!"{prefixMsg}: {formatDiagnostics diags fileMap}" + | .userError => + let userDiags := diags.filter (·.type == DiagnosticType.UserError) + let msg := match userDiags.head? with + | some d => formatUserErrorMessage d fileMap + | none => formatDiagnostics diags fileMap + exitPyAnalyzeUserError msg + | .knownLimitation => + let nyiDiags := diags.filter (·.type == DiagnosticType.NotYetImplemented) + let msg := match nyiDiags.head? with + | some d => d.message + | none => formatDiagnostics diags fileMap + exitPyAnalyzeKnownLimitation msg + +/-- Emit SMT `set-info` lines and write `user_errors.txt` for the first + user-code diagnostic in the batch. -/ +private def emitUserErrorsFile (diags : List DiagnosticModel) : IO Unit := do + let userDiags := diags.filter (·.type == DiagnosticType.UserError) + match userDiags.head? with + | none => pure () + | some d => + let filePath := match d.fileRange.file with | .file p => p + let range := d.fileRange.range + let mut lines := #[s!"(set-info :file {Strata.escapeSMTStringLit filePath})"] + unless range.isNone do + lines := lines.push s!"(set-info :start {range.start})" + lines := lines.push s!"(set-info :stop {range.stop})" + lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit d.message})" + for line in lines do + IO.println line + IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") + /-- Print the final RESULT/DETAIL lines based on solver outcomes. Always called on successful pipeline completion (as opposed to the exit helpers above, which are called on early pipeline failure). @@ -615,29 +674,10 @@ def pyAnalyzeLaurelCommand : Command where (quiet := quiet) (warningSummaryFile := warningSummaryFile) |>.toBaseIO with | .ok r => pure r - | .error (.userCode range msg) => - let location := if range.isNone then "" else - match mfm with - | some (_, fm) => - let pos := fm.toPosition range.start - s!" at line {pos.line}, col {pos.column}" - | none => "" - let filePath' := sourcePath.getD filePath - let mut lines := #[ - s!"(set-info :file {Strata.escapeSMTStringLit filePath'})" - ] - unless range.isNone do - lines := lines.push s!"(set-info :start {range.start})" - lines := lines.push s!"(set-info :stop {range.stop})" - lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit msg})" - for line in lines do - IO.println line - IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") - exitPyAnalyzeUserError s!"{msg}{location}" - | .error (.knownLimitation msg) => - exitPyAnalyzeKnownLimitation msg - | .error (.internal msg) => - exitPyAnalyzeInternalError msg + | .error diags => + emitUserErrorsFile diags + let fileMap := mfm.map (·.2) + classifyDiagnosticsAndExit "Python to Laurel translation failed" diags fileMap if verbose then IO.println "\n==== Laurel Program ====" @@ -656,7 +696,10 @@ def pyAnalyzeLaurelCommand : Command where let coreProgram ← match coreProgramOption with | none => - exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}" + emitUserErrorsFile laurelTranslateErrors + let fileMap := mfm.map (·.2) + classifyDiagnosticsAndExit "Laurel to Core translation failed" + laurelTranslateErrors fileMap | some core => pure core if verbose then diff --git a/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected new file mode 100644 index 0000000000..60a198ab8a --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected @@ -0,0 +1,6 @@ +(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py") +(set-info :start 69) +(set-info :stop 77) +(set-info :error-message "calls to procedures are not supported in functions or contracts") +DETAIL: calls to procedures are not supported in functions or contracts at line 5, col 22 +RESULT: User error diff --git a/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected new file mode 100644 index 0000000000..8ee60742df --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected @@ -0,0 +1,4 @@ +(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py") +(set-info :start 69) +(set-info :stop 77) +(set-info :error-message "calls to procedures are not supported in functions or contracts") diff --git a/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py b/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py new file mode 100644 index 0000000000..6937e78589 --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py @@ -0,0 +1,5 @@ +def helper() -> int: + return 0 + +def main(): + assert helper() < helper() < 10, "chained compare with procedure calls" diff --git a/StrataTest/Util/DiagnosticClassifier.lean b/StrataTest/Util/DiagnosticClassifier.lean new file mode 100644 index 0000000000..10839de362 --- /dev/null +++ b/StrataTest/Util/DiagnosticClassifier.lean @@ -0,0 +1,31 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +meta import Strata.Util.DiagnosticClassifier +import Strata.Util.DiagnosticClassifier + +open Strata + +def mkDiag (t : DiagnosticType) : DiagnosticModel := + { fileRange := FileRange.unknown, message := "test", type := t } + +-- Individual arms +#guard classifyDiagnostics [mkDiag .StrataBug] = .internalError +#guard classifyDiagnostics [mkDiag .UserError] = .userError +#guard classifyDiagnostics [mkDiag .NotYetImplemented] = .knownLimitation + +-- Priority: StrataBug > UserError > NotYetImplemented +#guard classifyDiagnostics [mkDiag .UserError, mkDiag .StrataBug] = .internalError +#guard classifyDiagnostics [mkDiag .StrataBug, mkDiag .UserError] = .internalError +#guard classifyDiagnostics [mkDiag .NotYetImplemented, mkDiag .UserError] = .userError +#guard classifyDiagnostics + [mkDiag .NotYetImplemented, mkDiag .UserError, mkDiag .StrataBug] = .internalError + +-- Defensive fallthrough +#guard classifyDiagnostics [] = .internalError +#guard classifyDiagnostics [mkDiag .Warning] = .internalError +#guard classifyDiagnostics [mkDiag .Warning, mkDiag .Warning] = .internalError From 88245df2949b103a747aae3676f0a6016e621e16 Mon Sep 17 00:00:00 2001 From: Jules Date: Wed, 6 May 2026 11:40:12 -0700 Subject: [PATCH 2/3] Register DiagnosticClassifier in Strata.lean Satisfies lake lint's requirement that every Strata module be transitively imported from the library root. --- Strata.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Strata.lean b/Strata.lean index b64f7abbd0..ad1019e907 100644 --- a/Strata.lean +++ b/Strata.lean @@ -17,6 +17,7 @@ import Strata.DL.Lambda.Lambda import Strata.DL.Imperative.Imperative /- Utilities -/ +import Strata.Util.DiagnosticClassifier import Strata.Util.NameProofs import Strata.Util.Sarif From 606892ae2942e60e0ce3c97230c490dba2ffa34c Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 12:13:44 -0700 Subject: [PATCH 3/3] Address review feedback on diagnostic unification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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. --- Strata/Languages/Python/PySpecPipeline.lean | 38 +++++------------ StrataMain.lean | 46 +++++++++------------ 2 files changed, 30 insertions(+), 54 deletions(-) diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index 36a18815d8..1fe1ec8dfe 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -390,35 +390,17 @@ public def translateCombinedLaurel (combined : Laurel.Program) let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined (profile := profile) return (coreOption, errors) -/-- 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 -using `classifyDiagnostics`. This type replaces the prior three-case -`PipelineError` inductive; routing is now driven by `DiagnosticType` rather -than by sum-type constructors, so the Python→Laurel and Laurel→Core pipeline -stages share a single classifier. -/ +/-- A batch of diagnostics emitted by the pyAnalyzeLaurel pipeline. Routing +to an exit category is driven by each entry's `DiagnosticType` via +`classifyDiagnostics`. -/ public abbrev PipelineError := List DiagnosticModel -/-- Helper: create a user-code error diagnostic. - -The optional `filePath`/`range` populate the `FileRange` used by -`classifyDiagnosticsAndExit` to format locations and by the -`user_errors.txt` side effect to emit SMT `set-info` lines. -/ public def mkUserCodeDiagnostic (filePath : String) (range : SourceRange) (msg : String) : DiagnosticModel := { fileRange := { file := .file filePath, range := range } message := msg type := .UserError } -/-- Helper: create a known-limitation diagnostic (intentionally unsupported). -/ -public def mkKnownLimitationDiagnostic (msg : String) : DiagnosticModel := - { fileRange := FileRange.unknown, message := msg, type := .NotYetImplemented } - -/-- Helper: create an internal-error diagnostic (tool bug). -/ -public def mkInternalDiagnostic (msg : String) : DiagnosticModel := - { fileRange := FileRange.unknown, message := msg, type := .StrataBug } - /-- Run the pyAnalyzeLaurel pipeline: read a Python Ion program, resolve overloads from dispatch files, load PySpec declarations, translate Python to Laurel, and combine with PySpec Laurel. @@ -445,17 +427,18 @@ public def pythonAndSpecToLaurel (warningSummaryFile : Option String := none) : EIO PipelineError Laurel.Program := do let metadataPath := sourcePath.getD pythonIonPath + let internalErr (msg : String) : PipelineError := + [DiagnosticModel.fromMessage msg (type := .StrataBug)] let stmts ← profileStep profile "Read Python Ion" do match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with | .ok r => pure r - | .error msg => throw [mkInternalDiagnostic msg] + | .error msg => throw (internalErr msg) let result ← profileStep profile "Resolve and build Laurel prelude" do match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir (quiet := quiet) |>.toBaseIO with | .ok r => pure r - | .error msg => throw [mkInternalDiagnostic msg] + | .error msg => throw (internalErr msg) - -- Print and write PySpec warnings before later stages can fail let pyspecWarnings := result.pyspecWarnings if pyspecWarnings.size > 0 && !quiet then let _ ← IO.eprintln @@ -488,14 +471,15 @@ public def pythonAndSpecToLaurel | .error (.userPythonError range msg) => throw [mkUserCodeDiagnostic metadataPath range msg] | .error (.unsupportedConstruct msg ast) => - throw [mkKnownLimitationDiagnostic s!"Unsupported construct: {msg}\nAST: {ast}"] - | .error e => throw [mkInternalDiagnostic s!"Python to Laurel translation failed: {e}"] + throw [DiagnosticModel.fromMessage s!"Unsupported construct: {msg}\nAST: {ast}" + (type := .NotYetImplemented)] + | .error e => throw (internalErr s!"Python to Laurel translation failed: {e}") | .ok result => pure result let filteredPrelude ← profileStep profile "Filter prelude" do match Laurel.filterPrelude result.laurelProgram laurelProgram with | .ok prog => pure prog - | .error msg => throw [mkInternalDiagnostic msg] + | .error msg => throw (internalErr msg) profileStep profile "Combine PySpec and user Laurel" do return combinePySpecLaurel filteredPrelude laurelProgram diff --git a/StrataMain.lean b/StrataMain.lean index 9446e7e210..43d1b6f3b1 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -526,44 +526,36 @@ private def formatUserErrorMessage (d : DiagnosticModel) (fileMap : Option Lean. | none => "" s!"{d.message}{location}" -/-- 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. -/ +/-- Classify `diags` and exit with the matching `pyAnalyzeLaurel` category. + `prefixMsg` is prepended only to internal-error details. -/ private def classifyDiagnosticsAndExit {α} (prefixMsg : String) (diags : List DiagnosticModel) (fileMap : Option Lean.FileMap) : IO α := do + let firstOf (t : DiagnosticType) (fmt : DiagnosticModel → String) : String := + match (diags.filter (·.type == t)).head? with + | some d => fmt d + | none => formatDiagnostics diags fileMap match classifyDiagnostics diags with | .internalError => exitPyAnalyzeInternalError s!"{prefixMsg}: {formatDiagnostics diags fileMap}" | .userError => - let userDiags := diags.filter (·.type == DiagnosticType.UserError) - let msg := match userDiags.head? with - | some d => formatUserErrorMessage d fileMap - | none => formatDiagnostics diags fileMap - exitPyAnalyzeUserError msg + exitPyAnalyzeUserError (firstOf .UserError (formatUserErrorMessage · fileMap)) | .knownLimitation => - let nyiDiags := diags.filter (·.type == DiagnosticType.NotYetImplemented) - let msg := match nyiDiags.head? with - | some d => d.message - | none => formatDiagnostics diags fileMap - exitPyAnalyzeKnownLimitation msg + exitPyAnalyzeKnownLimitation (firstOf .NotYetImplemented (·.message)) /-- Emit SMT `set-info` lines and write `user_errors.txt` for the first user-code diagnostic in the batch. -/ private def emitUserErrorsFile (diags : List DiagnosticModel) : IO Unit := do - let userDiags := diags.filter (·.type == DiagnosticType.UserError) - match userDiags.head? with - | none => pure () - | some d => - let filePath := match d.fileRange.file with | .file p => p - let range := d.fileRange.range - let mut lines := #[s!"(set-info :file {Strata.escapeSMTStringLit filePath})"] - unless range.isNone do - lines := lines.push s!"(set-info :start {range.start})" - lines := lines.push s!"(set-info :stop {range.stop})" - lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit d.message})" - for line in lines do - IO.println line - IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") + let some d := (diags.filter (·.type == DiagnosticType.UserError)).head? | pure () + let .file filePath := d.fileRange.file + let range := d.fileRange.range + let mut lines := #[s!"(set-info :file {Strata.escapeSMTStringLit filePath})"] + unless range.isNone do + lines := lines.push s!"(set-info :start {range.start})" + lines := lines.push s!"(set-info :stop {range.stop})" + lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit d.message})" + for line in lines do + IO.println line + IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") /-- Print the final RESULT/DETAIL lines based on solver outcomes. Always called on successful pipeline completion (as opposed to the