Formatting and debugging improvements#1115
Conversation
github-actions
Bot
added
Laurel
Python
github_actions
github-actions
Bot
added
Waiting-For-Review
and removed
github_actions
|
@keyboardDrummer-bot please resolve the build failures |
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
1. Scope. The PR title is accurate but understates what's inside. It contains:
- Formatter change in
Strata/DDM/Format.lean:456— flipsSepFormat.semicolonfrom"; "to";\n". This is a DDM-wide change that affects any dialect usingSemicolonSepBy. I searched the repo (grep -rn SemicolonSepBy Strata/Languages --include='*.st') and only Laurel currently uses it, so in practice the blast radius is the Laurel tests you're already updating — but the commit history doesn't flag this as a cross-cutting change, and anyone adding a new dialect that usesSemicolonSepBylater will inherit the vertical layout without necessarily expecting it. Worth a one-line PR-body note or a comment inFormat.lean. - Laurel grammar change at
LaurelGrammar.st:109–110— theblockandlabelledBlockops use"{\n " indent(2, stmts) "\n}"instead of the single-line form. This is the Laurel-local wrapper that, combined with (1), gives the vertical{ \n … \n}shape. - Diagnostic-reporting refactor in
LaurelToCoreTranslator.leanandLaurelCompilationPipeline.lean—Bool → List DiagnosticModel. Touches a different concern from the formatter change. - Test helper
processLaurelFileKeepIntermediatesinTestExamples.lean, plus.gitignoreentry forBuild/. - ~250 lines of test expected-output updates across 8+ files.
Ideally this would have been three PRs (formatter, diagnostic refactor, test helper). Given it's already cut, a structured commit log and PR body note would help reviewers separate the concerns — they're independently reviewable.
2. Silent-suppression edge case. At LaurelCompilationPipeline.lean:218:
if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then
let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown)
allDiagnostics := allDiagnostics ++ locatedDiags
let coreProgramOption :=
if !translateState.coreDiagnostics.isEmpty then none else coreProgramOptionIf translateState.coreDiagnostics is non-empty but every entry has FileRange.unknown, then:
locatedDiags = [], soallDiagnosticsstays empty.coreProgramOption := nonebecausecoreDiagnostics.isEmpty = false.- User sees: no diagnostics, but the translation is suppressed.
The intended rationale ("those without one are not actionable for the user") is understandable for locations, but the diagnostics still carry a message field that's strictly more useful than silence. Before this PR the behaviour was "silent suppression on coreProgramHasSuperfluousErrors = true", so this isn't a regression — it just misses an opportunity that the new design could take.
Two shapes of fix:
- Don't filter.
allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics. The user gets themessagetext without a location; still better than silence, and theStrataBugtype tag (which everyinvalidCoreTypeentry sets) already flags these as pipeline issues rather than user errors. - Fallback message. Keep the filter; if
locatedDiagsis empty butcoreDiagnosticsis non-empty, synthesise a single summary diagnostic of the form"Translation suppressed with {n} internal errors without source locations: {message1}; {message2}; …".
Inline suggestion on line 215–223.
3. Duplicate test helper. processLaurelFileKeepIntermediates (plus buildDir plus the Build/ .gitignore entry) is added verbatim by PR #1113 as well. Whichever lands first, the other will have a merge conflict. Worth coordinating with the #1113 author so only one PR lands the helper (probably this one, since the PR description ties it to the diagnostic-reporting debugging work).
4. invalidCoreType default reason is noisy. LaurelToCoreTranslator.lean:78:
private def invalidCoreType (source : Option FileRange := none) (reason : String := "Type could not be translated to Core (resolution error placeholder)") : TranslateM LMonoTy := doEvery call site now passes an explicit source and reason — the only caller left using the default is… none, I think; every invalidCoreType call site in this diff passes both arguments. If that's true, dropping the defaults makes the contract explicit and eliminates a class of "I forgot to say why" callers. Low-priority stylistic nit.
5. Redundant diagnostic write in the last arm of translateType. Lines 111–113:
| _ => do
emitDiagnostic (diagnosticFromSource ty.source "cannot translate type to Core: not supported yet" DiagnosticType.StrataBug)
invalidCoreType ty.source s!"cannot translate type to Core: not supported yet"The emitDiagnostic call adds the message to state.diagnostics; the invalidCoreType call then also constructs and appends an identical message to state.coreDiagnostics. Since allDiagnostics is now non-empty (the emitDiagnostic entry), the guard at line 215 skips over the coreDiagnostics entry — so the duplicate is dead state, not user-visible duplication, but it's carrying a second copy of the same DiagnosticModel through the pipeline. Either drop the emitDiagnostic (and rely on the fallback surfacing at line 218) or have invalidCoreType only append to coreDiagnostics without constructing a fresh diagnostic when the caller already emitted one. Small cleanup; not blocking.
| /-- Project-root-relative path to the `Build/` directory for intermediate files. | ||
| Resolved from the current working directory so it works on any machine. -/ | ||
| def buildDir : IO String := do | ||
| let cwd ← IO.currentDir | ||
| return s!"{cwd}/Build/" | ||
|
|
||
| def processLaurelFileKeepIntermediates (input : InputContext) : IO (Array Diagnostic) := do | ||
| let dir ← buildDir |
There was a problem hiding this comment.
Duplicate helper with PR #1113. The buildDir + processLaurelFileKeepIntermediates pair, and the .gitignore Build/ entry, are added verbatim by PR #1113 as well. Whichever of the two PRs lands first, the other gets a merge conflict on three files.
Secondary note: processLaurelFileKeepIntermediates isn't called from any test in this diff — it's infrastructure for ad-hoc debugging. That's fine, but infrastructure without a first caller tends to rot. If you have a specific debugging scenario the helper is intended for, consider wiring a small example test that actually uses it (asserting that Build/ gets populated, or just smoke-testing one pass's intermediate file).
Or, if the helper is strictly for local debugging and not intended to run in CI, mark it @[inline]-ish with a comment (-- For local debugging; never invoked in CI) and leave the .gitignore hint alone. Either way, some form of "why this exists" annotation would help the next maintainer who sees an unused public def.
Are you asking me to change my approach to cutting PRs? I'm not used to a PR like this, which is of fairly manageable size and complexity, to get such feedback.
Let's remove the filter. It makes no sense to me :) @keyboardDrummer-bot can you do that?
I don't think there would be a merge conflict, since the code is the same, and if there was, it would be trivially resolved by a bot. Do you really think coordination here (with the other author also being myself) is necessary?
Okay, @keyboardDrummer-bot please remove the default.
@keyboardDrummer-bot please remove the redundant write. |
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
LaurelCompilationPipeline.lean (my inline on lines 215–223; thread now marked resolved on GitHub). 0b6cee46 took my option (a) — dropping the filter — then b30607ea reverted it with message "Diagnostics without a known source location are not actionable for the user. Restore the filter to fix the T1_MutableFields test failure." So:
- The root concern (unlocated
coreDiagnosticsget silently dropped, the refactor's "we now have the info" promise is partially broken) still holds in the current code. - The test failure the revert cites reveals something I hadn't noticed: unlocated
coreDiagnosticsare being produced during the normal verification ofT1_MutableFields, not only in the "shouldn't happen" paths. That's itself a symptom of upstream diagnostic labeling being sloppier than the filter's rationale assumes. - Option (b) from my earlier inline — keep the filter but synthesise a summary diagnostic when
locatedDiagsis empty ANDcoreDiagnosticsis non-empty — wasn't tried. It wouldn't hit the test-failure that killed option (a), because inT1_MutableFields's case the located arm is active alongside any unlocated entries, so the fallback never fires. See the renewed inline.
The b30607ea revert commit message suggests unlocated coreDiagnostics fire during normal operation. If the T1_MutableFields test hits the surfacing path (which it would if allDiagnostics.isEmpty and any coreDiagnostics are present), then some upstream invalidCoreType call is recording a DiagnosticType.StrataBug diagnostic without a source location as part of a successful T1 compile. That's not something the filter can fix — it's a mislabelling at the source (an invalidCoreType call that shouldn't be firing, or firing without a source when one is available). Worth tracking as a follow-up: grep invalidCoreType Strata/Languages/Laurel/LaurelToCoreTranslator.lean against the T1 fixture to find which call site is the culprit.
No test or proof coverage changes from my earlier review — the suggestions I made there still apply, and the regression test I asked for would have caught exactly the case that drove the revert: a program whose suppression reason is a StrataBug without source location should emit something to the user, not silence.
| if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then | ||
| -- The program was suppressed but no diagnostics explain why — report the core diagnostics | ||
| -- that have a known source location (those without one are not actionable for the user). | ||
| let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown) | ||
| allDiagnostics := allDiagnostics ++ locatedDiags | ||
|
|
||
| let coreProgramOption := | ||
| if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption | ||
| if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption | ||
| return (coreProgramOption, allDiagnostics, program, stats) |
There was a problem hiding this comment.
Renewed concern. Thread #2 on this block was marked resolved but the revert at b30607ea restored the silent-suppression edge case I originally flagged. To recap:
0b6cee46took my option (a): drop the filter, surface allcoreDiagnostics. The T1_MutableFields test failed.b30607eareverted to the original filter, citing that test failure.- The silent-suppression case is therefore still present in the current HEAD.
The revert message notes "Diagnostics without a known source location are not actionable for the user." — fair, but the conclusion-from-test-failure isn't "drop them silently", it's "the current flood of unlocated diagnostics during T1's compile is surprising in the first place". Two independent follow-ups are worth doing:
In this PR — try option (b) from my earlier inline. Keep the filter, but when all the coreDiagnostics are unlocated, synthesise a single summary diagnostic so the user isn't left with silence:
| if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then | |
| -- The program was suppressed but no diagnostics explain why — report the core diagnostics | |
| -- that have a known source location (those without one are not actionable for the user). | |
| let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown) | |
| allDiagnostics := allDiagnostics ++ locatedDiags | |
| let coreProgramOption := | |
| if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption | |
| if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption | |
| return (coreProgramOption, allDiagnostics, program, stats) | |
| if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then | |
| -- Prefer located diagnostics; fall back to a single synthetic summary when | |
| -- every coreDiagnostic is unlocated, so the user always sees *some* | |
| -- explanation when translation is suppressed. | |
| let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown) | |
| if !locatedDiags.isEmpty then | |
| allDiagnostics := allDiagnostics ++ locatedDiags | |
| else | |
| let msgs := String.intercalate "; " (translateState.coreDiagnostics.map (·.message)) | |
| let summary : DiagnosticModel := { | |
| fileRange := FileRange.unknown, | |
| message := s!"Translation suppressed: {translateState.coreDiagnostics.length} internal errors without source locations — {msgs}", | |
| type := DiagnosticType.StrataBug } | |
| allDiagnostics := allDiagnostics ++ [summary] | |
| let coreProgramOption := | |
| if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption | |
| return (coreProgramOption, allDiagnostics, program, stats) |
This avoids the T1_MutableFields regression: T1 hits the "located diagnostics exist" branch, so the fallback never fires. It only fires in the genuinely-silent case my original review called out.
As a follow-up issue — investigate why T1 ever produces unlocated StrataBug diagnostics. If T1 is a known-good fixture, any diagnostic produced during its compile is a labeling bug (either a missed source range on an invalidCoreType call, or a pass that shouldn't be firing at all). The grep invalidCoreType Strata/Languages/Laurel/LaurelToCoreTranslator.lean sites are the place to start — each should either have a definite ty.source or a comment explaining why it's unsourceable. This is out of scope for this PR but worth filing.
Not blocking the merge — the current behaviour matches pre-PR silent-suppression semantics — but the option (b) fallback is a one-shape-fits-both improvement that's cheap and localised to this block.
keyboardDrummer
force-pushed
the
formatting-and-debugging-improvements
branch
from
20df9b0 to
7e34b04
Compare
| pure (.atom .nil) | ||
| else do | ||
| let f i q s := return s ++ "; " ++ (← entries[i].mformatM).format | ||
| let f i q s := return s ++ ";\n" ++ (← entries[i].mformatM).format |
There was a problem hiding this comment.
Nit: This seems adequate but it's a bit surprising that ".semicolon" does both semicolon + newline. If ";\n" is better, why not renaming to .semicolonNewline` so that its effect is not surprising?
There was a problem hiding this comment.
Note that the newline is not required for parsing. @keyboardDrummer-bot could you apply the requested rename?
| { | ||
| assert true; | ||
| assert false | ||
| }; |
There was a problem hiding this comment.
Nit: The newlines make it look much nicer! But I'm still surprised that the last statement does not end with a semicolon. This means that to add a statement, one has to add a semicolon at the end of a line, a newline and the new statement.
I would recomment using a NewlineSepBy instead if it's not ambiguous, and if it is ambiguous, require that a semicolon ends each statement.
Since I'm not the main designer of that dialect and the last statement was already formatted without a semicolon, I'll leave it to you.
There was a problem hiding this comment.
I agree that ending each statement in a block with a semicolon is probably better. I would prefer to leave that for a follow-up though.
About using NewlineSepBy, I think without the semicolons it would be ambiguous, although I'm not sure. In any case removing the semicolons is a change I would prefer to make in a follow-up.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🤖🔍 Overall a clean PR. The formatting changes are straightforward and the test updates are consistent. The coreDiagnostics refactoring is a nice improvement over the boolean flag — it gives much better debuggability. A couple of observations below.
| private def invalidCoreType : TranslateM LMonoTy := do | ||
| modify fun s => { s with coreProgramHasSuperfluousErrors := true } | ||
| private def invalidCoreType (source : Option FileRange) (reason : String) : TranslateM LMonoTy := do | ||
| modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ |
There was a problem hiding this comment.
🤖🔍 The pattern modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [..] } appears 5 times in this file. Consider extracting an emitCoreDiagnostic helper (analogous to emitDiagnostic) to reduce repetition and make the intent clearer.
There was a problem hiding this comment.
@keyboardDrummer-bot could you extract the pattern into emitCoreDiagnostic ?
| emitDiagnostic $ md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug | ||
| modify fun s => { s with coreProgramHasSuperfluousErrors := true } | ||
| let d := md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug | ||
| modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] } |
There was a problem hiding this comment.
🤖🔍 Behavior change: on main, this case called emitDiagnostic (unconditionally surfacing the diagnostic) AND set the flag. Now it only appends to coreDiagnostics, meaning the diagnostic is only surfaced when allDiagnostics is otherwise empty. Is this intentional? If another pass emits an unrelated warning, this "Return with value should have been eliminated" bug indicator will be silently dropped.
There was a problem hiding this comment.
This is fine. This diagnostic flags a bug so it's OK if it's hidden by other errors.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🤖🔍 The new commit (65ab6ae5) is a clean mechanical rename of SepFormat.semicolon → SepFormat.semicolonNewline — looks good.
However, my two previous inline comments remain unaddressed:
-
emitCoreDiagnostichelper — themodify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [..] }pattern still appears 5 times. Extracting a helper (analogous toemitDiagnostic) would reduce repetition. -
Behavior change in the
return-with-valuecase (line ~505) — onmainthis calledemitDiagnostic(unconditionally surfacing the diagnostic) AND set the flag. The current code only appends tocoreDiagnostics, meaning the diagnostic is only surfaced whenallDiagnosticsis otherwise empty. If another pass emits an unrelated warning, this bug indicator gets silently dropped.
Neither is blocking, but worth addressing before merge. Reviewer sign-off still needed.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🤖🔍 Comment #1 (extract emitCoreDiagnostic helper) is fully addressed in commit 5c0a458 — all 5 occurrences now use the helper.
Comment #2 (behavior change in the return-with-value case): the case at line ~507 still only calls emitCoreDiagnostic d without also calling emitDiagnostic d, unlike throwStmtDiagnostic which does both. This means the diagnostic won't surface unconditionally if other diagnostics exist. If this is intentional (StrataBug diagnostics shouldn't clutter user-facing output), a brief comment explaining the choice would help future readers. Not blocking.
Reviewer sign-off still needed.
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
Only one remaining gap from my original review (has not been addressed so far):
No regression test for the silent-suppression case. The point of the Bool → List DiagnosticModel refactor is precisely that we now have the information that was previously thrown away. A 10-line test that constructs a Laurel input forcing invalidCoreType to fire (e.g. via a synthesised HighTypeMd whose .val matches the catch-all arm of translateType) and asserts that processLaurelFile's returned diagnostics list is non-empty would lock the contract in. Without it, a future simplification of lines 220–224 — particularly any reintroduction of the FileRange.unknown filter — silently re-introduces the silent suppression, and CI won't notice.
Proof opportunities (none currently exist for these helpers):
theorem emitCoreDiagnostic_appends (d s) : ((emitCoreDiagnostic d).run s).snd.coreDiagnostics = s.coreDiagnostics ++ [d]— trivial but pins the contract thatemitCoreDiagnosticis purely append-only (it currently is, but a future O(1) prepend-and-reverse refactor could change that).theorem coreDiagnostics_nonempty_iff_suppressed : translateState.coreDiagnostics ≠ [] ↔ translateLaurelToCore returns none ∨ pipeline surfaces them— formalises the suppression invariant the inline above relies on. Probably too much wiring for this PR; worth a follow-up.
| if let some coreProgram := coreProgramOption then | ||
| emit "CoreProgram" "core.st" coreProgram | ||
| let mut allDiagnostics := passDiags ++ translateState.diagnostics | ||
|
|
There was a problem hiding this comment.
Style nit: the guard uses .length > 0 here but !.isEmpty two lines below for the same check. Pick one (!translateState.coreDiagnostics.isEmpty matches the rest of the file and avoids the linear-time .length call). Not blocking.
4 participants
Summary
Extracts the formatting and debugging improvements from #34 into a standalone PR.
Formatting improvements
{ stmt1; stmt2 }to vertical layout withindent(2):Debugging improvements
coreProgramHasSuperfluousErrorswith acoreDiagnostics : List DiagnosticModelthat records why the Core program was suppressed. When no other diagnostics explain the suppression, these are surfaced to the user.invalidCoreType: Addssourceandreasonparameters so each suppression site provides context about what went wrong.processLaurelFileKeepIntermediatestest helper that writes pipeline intermediate files toBuild/for debugging..gitignore: AddsBuild/directory.Test updates
#guard_msgswhitespace fixes.opaquekeyword where needed for the new formatting to apply correctly.