From 792e14b3678c5d858793e1031bc36a42068a26c3 Mon Sep 17 00:00:00 2001 From: Massart Date: Tue, 5 May 2026 09:50:11 -0700 Subject: [PATCH 1/2] pyAnalyzeLaurel: classify UserError diagnostics as known limitations When Laurel-to-Core translation fails, pyAnalyzeLaurel previously reported every failure as 'RESULT: Internal error' (exit 3), including legitimate user-facing limitations such as 'calls to procedures are not supported in functions or contracts'. These are UserError-level diagnostics; reporting them as internal errors conflates genuine compiler bugs with 'not yet supported' constructs. Classify by diagnostic type: only StrataBug triggers 'Internal error'. UserError and NotYetImplemented trigger 'Known limitation' (exit 4). If the batch contains both a StrataBug and a UserError, the Strata bug takes priority so real compiler issues are not hidden. --- StrataMain.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/StrataMain.lean b/StrataMain.lean index 179d04a6c0..f5a523ebc7 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -656,7 +656,15 @@ def pyAnalyzeLaurelCommand : Command where let coreProgram ← match coreProgramOption with | none => - exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}" + let msg := s!"Laurel to Core translation failed: {laurelTranslateErrors}" + let hasStrataBug := laurelTranslateErrors.any + (fun d => d.type == DiagnosticType.StrataBug) + -- If any diagnostic is a StrataBug, treat the whole failure as internal + -- (a Strata bug takes priority over known limitations). + if hasStrataBug then + exitPyAnalyzeInternalError msg + else + exitPyAnalyzeKnownLimitation msg | some core => pure core if verbose then From 4708b82a38f38e03e4475c1c84e386c520483cbf Mon Sep 17 00:00:00 2001 From: Jules Massart <68219272+julesmt@users.noreply.github.com> Date: Tue, 5 May 2026 10:13:11 -0700 Subject: [PATCH 2/2] Michael's suggestion 1 Co-authored-by: Michael Tautschnig --- StrataMain.lean | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/StrataMain.lean b/StrataMain.lean index f5a523ebc7..5ffcf348a8 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -657,14 +657,20 @@ def pyAnalyzeLaurelCommand : Command where match coreProgramOption with | none => let msg := s!"Laurel to Core translation failed: {laurelTranslateErrors}" - let hasStrataBug := laurelTranslateErrors.any - (fun d => d.type == DiagnosticType.StrataBug) - -- If any diagnostic is a StrataBug, treat the whole failure as internal - -- (a Strata bug takes priority over known limitations). - if hasStrataBug then + -- Classify by worst-severity diagnostic: StrataBug (tool bug) outranks + -- UserError (user-actionable) outranks NotYetImplemented (wait-for-support). + -- An empty list or warnings-only failure with `coreProgramOption = none` + -- is itself a tool bug (translation should not silently fail). + if laurelTranslateErrors.isEmpty + ∨ laurelTranslateErrors.any (·.type == .StrataBug) then exitPyAnalyzeInternalError msg - else + else if laurelTranslateErrors.any (·.type == .UserError) then + exitPyAnalyzeUserError msg + else if laurelTranslateErrors.any (·.type == .NotYetImplemented) then exitPyAnalyzeKnownLimitation msg + else + -- Only warnings, but translation failed → unexpected. + exitPyAnalyzeInternalError msg | some core => pure core if verbose then