Wrap the Verification panel at spaces and operators, one conjunct per line by CatarinaGamboa · Pull Request #189 · liquid-java/vscode-liquidjava

CatarinaGamboa · 2026-11-10T18:57:37Z

Closes #187

What changes

The Verification panel's Expected box and every Found line:

One line per top-level conjunct, with && at the end of each line except the last. An && inside parentheses or a string literal stays on its line. Nothing is split when a weaker operator (||, -->, ?:) sits outside the parentheses, so a line never looks like a conjunct of the whole expression.
A conditional outside parentheses shows its condition on one line and each branch on an indented line of its own (? …, : …). This is what makes A1_09 fit.
Wrapped lines have a hanging indent, so you can see where each line starts.
No breaks inside names. The VC cells used overflow-wrap: anywhere, which gave failures.siz|e(), compressionN|otExplicit and display(host|) ==. They now use break-word, so a line breaks at a space and splits a name only when the name alone is wider than the line.
Narrow panel (webview at most 420 px wide). Each binder (∀host) goes above its predicate, so the predicate gets the whole width. The card and the Found box get less horizontal padding, and the Found lines get line-height 1.4 instead of 1.6.

This is display only. The text of every expression is the same as before, only laid out on more lines. The hover and the CLI do not change.

Acceptance check: the six study tasks at the study width

Headless VS Code at 1600×900, Dark Modern, default side bar (300 px; the error card is about 240 px). Verifier 0.0.37, the released one, which is what this branch builds with. Each image shows main on the left and this PR on the right. The webview is 794 px tall. "Found ends at" is the bottom of the Found box, in webview px.

Task	Found ends at (main → PR)
A2_10	503 → 453
A1_38	575 → 544
A1_01	562 → 521
A2_04	413 → 414
A1_56	498 → 473
A1_09	996 → 740: on main it ran below the fold

Expected and Found are fully visible in all six, with no name broken.

A1_09	A1_01

A2_10	A1_38

A2_04	A1_56

Verifier version

None needed. This works with 0.0.37 and with main.

Overlap with open PRs

List Found as facts and show only readable simplification steps #185 (Found as facts) may conflict. It splits each Found node into conjunct lines in vc-changes.ts (formatImplicationLines, with its own splitConjuncts), and this PR changes renderVCLine in the same file.
- The two are compatible: this PR's split keeps a trailing &&, so a line List Found as facts and show only readable simplification steps #185 has already split is left as it is.
- Whichever lands second should keep one splitConjuncts. This PR's copy is in highlighting.ts and follows the same rules.
- List Found as facts and show only readable simplification steps #185's binder-hiding on continuation lines works with the stacked binder layout.
Show the Context tab's refinements as the error messages show them #186 (Context tab): no overlap. This PR does not touch the Context tab or sections.ts.

Not changed

The Locations links (file names such as E_OSS_A1_01_SlideRecode|r.java) still break anywhere. They are in a <pre> with break-word, and the names are wider than the card. This was outside the issue.
Top-level || (A1_01's Expected) is not split into lines. The issue asks for conjuncts.

Checks

npm run test:unit (127 passed; 3 new tests, each fails on main), npm run test:typecheck, npm run lint, server mvn -B test (39 passed, unchanged).

🤖 Generated with Claude Code

CatarinaGamboa · 2026-11-10T18:59:51Z

Clean-code review

I audited this diff with the clean-code-principles checklist.

Fixed

highlighting.ts: splitConjuncts and getExpressionLines were exported but are only used inside the module, so they are module-private now (encapsulation, YAGNI).
renderHighlightedLines: the join("</span>") trick that closed spans is gone. Each line is now built explicitly, with the trailing arrow on the last line (KISS).

Declined

DRY with List Found as facts and show only readable simplification steps #185's splitConjuncts in vc-changes.ts. Both PRs are open, so the duplicate goes away when the second one lands, with one copy kept (noted in the body).
renderVCLine has two branches that both wrap in <span class="vc-node">. Merging them would move the arrow inside the animated diff highlight of changed lines, which would change how those look.
The 420px breakpoint is a literal, as the other breakpoints in styles.ts are. A CSS comment says what it is for.

CatarinaGamboa · 2026-11-10T19:05:06Z

Codex review, round 1

codex exec review --base origin/main:

[P2] Exclude character literals when locating conditional operators (highlighting.ts). In flag ? c == ':' : d, the colon inside ':' was taken for the conditional's separator.
[P2] Apply line formatting to changed VC predicates (vc-changes.ts). After stepping through the simplifications, a predicate that a step changed was rendered from its diff-highlighted HTML on one line, bypassing the line split.

Fixed (both)

topLevelIndices now skips single-quoted literals, with escapes, as well as strings. The existing line-split test covers it with c == ':'.
renderVCLine now takes a function that renders the text of each line, instead of finished HTML. A changed predicate is split into lines first, and each line is diffed against the old predicate. Whether the line counts as changed is decided on the whole predicate, as before. The two branches of renderVCLine are now one, which also clears the clean-code point I had declined. New test: keeps a conjunct per line in a predicate that a simplification changed.

Tests: 127 unit, typecheck, lint, and 39 server tests pass.

CatarinaGamboa · 2026-11-10T19:08:05Z

Codex review, round 2

[P2] Preserve change highlighting for repeated conjuncts (vc-changes.ts). Each line was diffed against the whole previous predicate. So for x > 0 becoming x > 0 && x > 0, the added x > 0 was not highlighted, because its tokens matched the old predicate.

Fixed. A changed predicate is now split into lines on both sides. The old and new lines are paired with the same alignChangedLines that pairs the lines of the chain. Each new line is diffed against the old line it replaces, and a new line that replaces none is highlighted whole. The test …marking a repeated conjunct it adds uses Codex's example and fails on round 1's code.

Tests: 127 unit, typecheck, lint, and 39 server tests pass.

CatarinaGamboa · 2026-11-10T19:09:30Z

Codex review, round 3

codex exec review --base origin/main: "I found no actionable regression in the changed code. The relevant unit tests pass."

The loop ends here: nothing to fix.

… line Expected and every Found line now show one top-level conjunct per line, and a conditional's condition and branches each on a line of their own, with a hanging indent for wrapped lines. The VC cells no longer break anywhere, so a name is split only when it alone is wider than the line. A narrow panel puts each binder above its predicate, with tighter padding and line height. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…erals Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Closes #188 ## What changes The editor diagnostic that `LJDiagnosticsHandler` publishes now carries: 1. the headline (`<title>: <message>`), as before; 2. then each of the verifier's **message notes**, `LJDiagnostic.getMessageNotes()`, one per line; 3. then the verifier's **counterexample**, `getCounterexampleStr()`, when it has one. That text is what the hover and the Problems view show. **Hints are left out**, since they stay collapsed in the panel by design. The server reads the verifier's generic `LJDiagnostic` API, not a per-error list. So any note the verifier adds later appears in the hover with no extension change. That includes the planned From note (liquid-java/liquidjava#522), and a counterexample for state errors once the verifier gives one. ## Before → after (hover text, verifier 0.0.37) **A2_04** ```diff Refinement Error: expected timeout >= 0 but could not prove it + Counterexample: timeout == -1 ``` **A2_10** ```diff Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0 + Counterexample: failures.size() == 0 ``` A1_38, A1_01, A1_56 and A1_09 are unchanged. Their errors have no message notes and no counterexample in 0.0.37 or main. | | Before | After | |---|---|---| | A2_04 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_04-before.png" width="440"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_04-after.png" width="440"> | | A2_10 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_10-before.png" width="440"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_10-after.png" width="440"> | (Headless VS Code, 1600×900, Dark Modern.) ## Verifier version **0.0.37**, already released. `getMessageNotes()` and `getCounterexampleStr()` are both in it, and the branch builds with the current pom. Today the only message notes are the `where <alias> means …` lines of refinement errors that use aliases, and no study task has one. The From note will come with a later verifier release. ## Open question for the PM The issue lists the `where … means …` gloss among the notes. In the verifier, the gloss is a **declaration note** (`getDeclarationNotes()`, liquid-java/liquidjava#517, needs 0.0.38). It explains the "declared here" excerpt, which the hover does not show. So this PR shows only the message notes, as specified. If the hover should also show the gloss, that is one more `lines.addAll(diagnostic.getDeclarationNotes())`, but it needs the 0.0.38 bump that #191 makes. ## Overlap with open PRs Server only, in `LJDiagnosticsHandler`. No conflict with #185, #186, #189 or #191. ## Checks Server `mvn -B test` (40 passed; new `LJDiagnosticsHandlerTest`, which fails on main), `npm run test:unit` (124 passed), `npm run test:typecheck`, `npm run lint`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Closes #181 ## What changes - **Server.** `RefinementErrorDTO` and `StateRefinementErrorDTO` now send: - `declarationPositions`, from `LJDiagnostic.getDeclarationPositions()`; - `declarationNotes`, the `where … means …` lines, from `getDeclarationNotes()`. Both are read through the verifier's generic `LJDiagnostic` API. So when the verifier adds notes or positions, they appear with no extension change. `declarationPosition`, the first position, stays as it is for the State Machine view. - **Client.** The Locations section links to **every** declaration position, then shows the notes under the links, muted and with a hanging indent. A declaration in value form (`doorState(this) == closed`), or one with unnamed sets, has no notes, so nothing changes for it. - **Fallback to one position.** The verifier's default `getDeclarationPositions()` returns the single `getDeclarationPosition()`. Refinement errors and any other error with one declaration therefore show one link, as before. ## Verifier version: needs 0.0.38 (not yet released) | Part | Verifier change | |---|---| | `declarationNotes` (the gloss) | liquid-java/liquidjava#517 (merged in main) | | `declarationPositions` (every `from`, e.g. A1_01 lines 110 and 111) | liquid-java/liquidjava#525 (**open**) | The pom is bumped to `0.0.38`, so **CI's server build fails until 0.0.38 is on Maven Central**. Please merge this PR only after a verifier release that has both #517 and #525. If #525 is not merged, drop the `declarationPositions` lines from the two DTOs (one line each) and use `declarationPosition` in `renderLocation` again. The gloss part only needs #517. I tested it locally against #525's head (`9d1bb1e`, which contains main), installed as 0.0.38 in an isolated Maven repository. ## Before → after (Locations section, at the study width) Before is main, with its server built on verifier main. After is this PR on #525's head. Headless VS Code, 1600×900, Dark Modern, default side bar. **A1_01**: both `from`s, each with its gloss ```diff E_OSS_A1_01_SlideRecoder.java:136 ImageWriteParamRefinements.java:110 + ImageWriteParamRefinements.java:111 + where compressionExplicit(this) means compression(this) == compressionExplicit + where compressionTypeSet(this) means compression(this) == compressionTypeSet ``` **A1_38** ```diff E_OSS_A1_38_FormatReaderManager.java:157 BufferedInputStreamRefinements.java:81 + where marked(this) means markState(this) == marked, open(this) means stream(this) == open ``` **A1_56**: `+ where redoable(this) means redoState(this) == redoable` **A1_09**: `+ where notDisplayable(this) means display(this) == notDisplayable` **A2_04**: unchanged. `@Refinement("_ >= 0")` has no gloss. The missing Hint in the after shot comes from #525, not from this PR. | A1_01 | A1_38 | |---|---| | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_01.png" width="420"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_38.png" width="420"> | | A1_56 | A1_09 | |---|---| | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_56.png" width="420"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_09.png" width="420"> | <details><summary>A2_04</summary> <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A2_04.png" width="420"> </details> The A1_01 and A1_09 shots are scrolled to Locations. The yellow outline is the focus left on Hints by the screenshot script. ## Overlap with open PRs - **#186 (Context tab)** may conflict in `client/src/webview/views/sections.ts`. It changes `renderVariableHighlightButton` and the imports, right after `renderLocation`, which this PR edits. - **#185 (Found as facts)** may conflict in `client/src/types/diagnostics.ts`. Both PRs add fields to `RefinementError` and `StateRefinementError`, in nearby hunks. No conflict in logic. - **#189 (panel wrapping)**: the notes are in the Locations `<pre>`, which keeps `break-word`, so a long `compressionExplicit(this)` can still wrap inside the name at 240 px (see A1_01). They do not share files apart from `styles.ts`, in separate rules. ## Checks `npm run test:unit` (125 passed; the new test fails on main and also checks the copied text), `npm run test:typecheck`, `npm run lint`, server `mvn -B test` (39 passed, against #525 as 0.0.38; the converter test now also checks the notes and the positions). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…194) Fixes the integration failure on main after #191 (stable) and the earlier ones on #189 (minimum) and #193 (both). Each time it was the same test timing out: `smoke.test.ts` › "activates, becomes ready, and verifies its isolated fixture". ## Cause The server only verifies when the first file of the workspace is opened (`LJDiagnosticsService.didOpen`). In the `failing` fixture, `state-errors.test.ts` runs first and opens and verifies the fixture. The smoke test then opens `FailingRefinement.java` and waits for a verification that the server never starts. It passed only when a late notification from the earlier test happened to arrive while it waited, which is why it failed on some runs and VS Code versions and not others. ## Change The smoke test waits for the verification on open only when the fixture has not been verified yet. It still runs the manual `liquidjava.verify` and checks its result as before. ## Tests - With a 5 s pause at the start of the smoke test, so every earlier notification has arrived: main times out exactly as in CI; this branch passes. - Without the pause: `xvfb-run -a npm test` (VS Code 1.82, the minimum) passes twice in a row, 9 + 1 tests; `test:typecheck` and `lint` pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…name (#193) Closes #192 **Stacked on #191** (base `feat/181-declaration-notes`): it renders #191's declared-here gloss, and it needs the same 0.0.38 bump. Retarget this PR to `main` before #191 is merged with `--delete-branch`. ## What changes **Server** - `LJDiagnosticDTO` now sends two more fields for every diagnostic: - `messageNotes`, from `getMessageNotes()`; - `references`, from `getReferences()`, as `SourceReferenceDTO(message, text, start, position)`. The position counts lines and columns from 0, like the other DTO positions. - Both come from the verifier's generic `LJDiagnostic` API. New notes and references therefore show up with no extension change. **Panel (Verification tab)** - The **message notes**, e.g. `Origin: line 134, …`, are shown under Found and the Counterexample. Before this PR the panel did not show notes at all. - Every message line goes through one renderer, `webview/message-text.ts`: the header message, notes, hints and the declared-here gloss. - **Code** the verifier marks with backticks is shown in the editor font, without the backticks, with VS Code's inline-code colours (`textPreformat`). - Spans are parsed as the verifier's `Code.render` parses them: the same run-of-backticks pattern, and one space of padding stripped. - **Each reference** (`line 134`, `ArrayListRefinements.java:162`) is a link that opens that file at that line. It is placed at the reference's `start`; the text is not searched for, as the verifier asks. It reuses the panel's existing `location-link` handler. - **Hints** are now in the UI font, so their code stands out. Before, the whole hint was monospace. - **Header message:** it is now escaped. Before, it was put into the HTML unescaped. **Hover and Problems:** unchanged by this PR. See the two options below. ## Verifier version Needs a release (0.0.38 or later) containing **liquid-java/liquidjava#528, #530 and #533**, on top of #517 and #525 (both on main). - `getReferences()`, `SourceReference` and the backticks come from #533. - The Origin notes come from #528/#530. I tested against #533's head (`1e94930`), installed as 0.0.38 into an isolated Maven repository. Like #191, CI's server build fails until 0.0.38 is on Maven Central. ## Panel at the study width: before (#191) → after (this PR) Both use verifier #533, with Hints open. The notes are new, the code is set apart, and `line 134` is a link. | A1_38 | A2_10 | |---|---| | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38.png" width="420"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_10.png" width="420"> | | A2_04 | A1_56 | |---|---| | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_04.png" width="420"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_56.png" width="420"> | | A1_01 | A1_09 (hints) | |---|---| | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01.png" width="420"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_09.png" width="420"> | **Clicking `line 134`** in A1_38 opens line 134, `new BufferedInputStream(stream)`: <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-link.png" width="860"> Panel text of the notes (verifier #533): ``` A1_38 Origin: line 134, new BufferedInputStream(stream) makes markState(buffered) == unmarked A1_01 Origin: line 130, writer.getDefaultWriteParam() returns compression(wParam) == compressionNotExplicit A2_04 Origin: line 94, timeout is a parameter of checkCimReachable(String, int) with no refinement A2_10 Origin: ArrayListRefinements.java:162, failures.size() guarantees only failures.size() >= 0 A1_56 Origin: line 69, frame.getUndoManager() says nothing about redoState(undoManager) ``` A1_09 has no Origin note. ## Hover: the two options VS Code shows a diagnostic's message as plain text. So the diagnostic hover and the Problems view keep the backticks. - **A, plain text (#190):** the diagnostic message is the headline, then the notes, then the counterexample, all plain with backticks, as rustc writes them. One text, the same as the CLI with colour off, in the hover and in Problems. - **B, markdown provider (prototype on branch `proto/192-markdown-hover`, not in this PR):** - The diagnostic message stays the headline only, as on main. - The extension's `HoverProvider` adds a markdown block with the notes and the counterexample: code spans, and `line 134` as a link. - VS Code draws it under the problem part, so nothing is shown twice. That holds only as long as #190's notes are not also in the diagnostic message. | | A: plain (#190 + #533) | B: markdown provider | |---|---|---| | A1_38 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-hover-a.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-hover-b.png" width="430"> | | A2_04 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_04-hover-a.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_04-hover-b.png" width="430"> | | A2_10 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_10-hover-a.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_10-hover-b.png" width="430"> | | A1_01 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01-hover-a.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01-hover-b.png" width="430"> | **Recommendation: A for the study.** - **Same text everywhere.** The hover is the one surface the baseline shares, and the joint review's decision 5 says compared elements must be in the hover/CLI text. A gives one string: hover = Problems = CLI with colour off. - **B splits the message.** It shows the message in two hover parts with two styles: the headline plain with backticks, the notes styled. The Problems view also loses the notes. - **B reads better on its own:** the code is set apart, and the cause is one click away. It is a good candidate after the study. Moving to it means taking the notes back out of #190's diagnostic message, so the two must not both be merged. ## Overlap with open PRs - **#191:** the base of this PR. - **#186** may conflict in `sections.ts`: both change the imports at the top. - **#189** may conflict in `errors.ts` (imports, and next to the Expected lines) and in `styles.ts` (separate rules, so unlikely). - **#185:** probably no textual conflict. It edits `LJErrorDTO` and the error types in `types/diagnostics.ts`; this PR edits `LJDiagnosticDTO` and `BaseDiagnostic`. - **#190:** no conflict in files. It is option A of the hover (above). ## Checks `npm run test:unit` (126 passed; the new panel test fails on the base), `npm run test:typecheck`, `npm run lint`, server `mvn -B test` (40 passed, against #533 as 0.0.38; the new converter test fails on the base). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Closes #183. Closes #176. ## What changes The **Found** box of the Verification tab gets plain step headers and, when the verifier could not prove Expected, a Summary step. Every step the verifier sends stays reachable with the arrows, as the PM decided: "Let's show it all, we will work on those identifiers after." - **The chain stays, one conjunct per line, from #189.** The `∀x` column (each binder still links to its source line) and the `→` arrows are kept, as the PM asked. The line layout comes from main's #189 (`getExpressionLines`): one top-level conjunct per line, and a conditional's branches on indented lines. This PR does not split anything itself. - **"Could not prove it" says so, one step ahead.** When the verifier's message ends with *expected … but could not prove it* (A1_56, A2_04), Found opens on a *Summary* step that reads *Nothing is known here that could prove Expected.* This is the wording of the verifier's Unknown category. The `←` arrow goes back to the newest step, e.g. `∀undoManager undoManager == #getUndoManager_result`, also when there was only one step. - **Every step is shown.** Found shows every step of the verifier's derivation, oldest (*Original*) to newest, plus the Summary when there is one. Older steps whose facts use generated names (`#if_condition`, `#switch_selector`, `extended#1`) are shown too, as are runs of the same pass, one step per pass. - **Step header (#176, per the PM's decision there).** The header shows *Original*, *Simplified*, or the name of a display step such as *Relevant to Expected*. An (i) icon after it gives a plain-language tooltip of what that step changed, e.g. "Replaced variables with the values they are equal to." Raw pass names (`Binder`, `Substitution`) are no longer shown. The tooltips cover every pass verifier 0.0.38 names: Substitution, Function Substitution, Binder, **Known Enum Values**, Folding, Arithmetic, Logical, Constraint, and the display step Relevant to Expected. Steps on the six study exercises (main → this PR). Each count is the verifier's own step count, plus one for the Summary: | Exercise | main | this PR | |---|---|---| | A1_56 (could not prove it) | 19 | 20 (Summary + 19) | | A2_04 (could not prove it) | 6 | 7 (Summary + 6) | | A1_09 | 10 | 10 | | A1_01 | 7 | 7 | | A1_38 | 4 | 4 | | A2_10 | 3 | 3 | **No step repeats the one before it.** The verifier records a step only when a pass changes the chain (`VCSimplification.simplifyOnce` returns the same result when the chain is equal). So the client needs no check for identical steps. A step can still look the same as the one before when the pass only changed a row Found does not draw, such as `∀#if_condition true →`. Such a step is shown anyway. ## Changes in this rework - **Every step is shown (PM's decision).** The filter that hid older steps with generated names is removed. So are the merging of runs of the same pass into one step and the de-duplication of steps that looked like the step before. Its code (`getVCSteps`, `sameLines`, `GENERATED_NAME`) and its test are gone, and `vc-changes.ts` is back to main. Before this rework, A1_56 showed the Summary and 1 step, A1_09 1 step, A1_01 2 and A1_38 1. - **Generated names are left for later.** `#if_condition`, `#switch_selector` and instance tags like `extended#1` now show in the older steps. #175 (line tags) and #195 (hover explanations) will handle them. - Earlier in this rework: rebased on main (verifier 0.0.38, #189, #190, #191, #186). The Summary is keyed on the message, not on `errorCategory` (see below), so **this PR is client-only**. ## Why the client, not the verifier The verifier's messages already leave generated names out: the hover of all six study exercises reads fine. The header and Summary only change how the view presents the steps the verifier sends. ## Screenshots (headless VS Code, light theme, verifier 0.0.38) Before: main (e333873). After: this branch (af43c9c). **A1_56** (could not prove it) | Before (19 steps) | Before, oldest step | After: opens on the Summary (20/20) | After, one step back (19/20) | After, oldest step (Original, 1/20) | |---|---|---|---|---| | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-before-oldest-step.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after-back.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after-oldest-step.png) | **A1_09** (path condition and state) | Before (10 steps) | After: Relevant to Expected (10/10) | After, one step back (9/10) | After, oldest step (1/10) | |---|---|---|---| | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after-back.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after-oldest-step.png) | **A2_10** (refinement error, three steps on both) | Before | After, Simplified 3/3 | After, Original 1/3 | |---|---|---| | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-after-original.png) | <details><summary>A1_01, A1_38, A2_04</summary> | | Before | After | After, one step back | After, oldest step | |---|---|---|---|---| | A1_01 (7 steps) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after-back.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after-oldest-step.png) | | A1_38 (4 steps) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after-back.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after-oldest-step.png) | | A2_04 (Summary + 6) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after-back.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after-oldest-step.png) | </details> ## For the PM - **When should the Summary show?** It is keyed on the message ending in *but could not prove it*, not on `errorCategory`. In 0.0.38 the two differ for some state errors. For example, if Found states only a non-state ghost of the receiver (`size(b) > 0`), the category is `unknown` but the message reads *found `size(b) > 0` but expected `open(b)`*. The message is what the hover shows, so it decides here. For refinement errors they agree, as they do on all six study exercises. Is keying on the message right? ## Tests `vc-implications.spec.ts` has two tests, each failing on main: - every step of the verifier is shown, including an original chain with `#if_condition` and two Binder steps in a row, each under *Original*, *Simplified* or *Relevant to Expected* with its tooltip (it also fails on the previous head, 55510f8, which hid these steps); - the Summary when the message says *could not prove it*, with the chain one step back. The test for skipping steps with generated names and merging pass runs is removed with that code. Local results on af43c9c: `npm run test:unit` (134 passed), `test:typecheck`, `lint`, server `mvn -B package` (42 tests), integration `xvfb-run -a npm test` on VS Code 1.82.0 (minimum; 9 + 1 passing). Codex review of this rework: one round, whose only finding (the Summary keyed on the message) was declined as in rounds 1 and 2. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa added a commit that referenced this pull request Nov 10, 2026

Screenshots for #189, #190 and #191

1e1c610

This was referenced Nov 10, 2026

Show the message notes and the counterexample in the hover #190

Merged

Show every declared-here position and its gloss in the IDE panel #191

Merged

CatarinaGamboa mentioned this pull request Nov 10, 2026

Show the code of messages in the editor font and link the lines they name #193

Merged

CatarinaGamboa and others added 3 commits November 11, 2026 14:22

Split changed Found predicates into lines too, and skip character lit…

c6a9aac

…erals Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Diff each line of a changed Found predicate against the line it replaces

79c1800

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa force-pushed the feat/187-panel-wrap branch from 600f884 to 79c1800 Compare November 11, 2026 14:29

CatarinaGamboa merged commit c218968 into main Nov 11, 2026
2 of 3 checks passed

CatarinaGamboa mentioned this pull request Nov 11, 2026

Smoke test: do not wait for a verification the server does not start #194

Merged

CatarinaGamboa mentioned this pull request Nov 11, 2026

List Found as facts and show only readable simplification steps #185

Merged

Navigation Menu

Repository navigation

Wrap the Verification panel at spaces and operators, one conjunct per line - #189

Wrap the Verification panel at spaces and operators, one conjunct per line#189
CatarinaGamboa merged 3 commits into
mainfrom
feat/187-panel-wrap

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

CatarinaGamboa commented Nov 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changes

Acceptance check: the six study tasks at the study width

Verifier version

Overlap with open PRs

Not changed

Checks

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Clean-code review

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 1

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 2

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 3

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading