Show every declared-here position and its gloss in the IDE panel by CatarinaGamboa · Pull Request #191 · liquid-java/vscode-liquidjava

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

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 froms, each with its gloss

  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

  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

A1_56	A1_09

A2_04

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

Show the Context tab's refinements as the error messages show them #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.
List Found as facts and show only readable simplification steps #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.
Wrap the Verification panel at spaces and operators, one conjunct per line #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

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

Clean-code review

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

Fixed

renderLocation reads the positions and the notes from one narrowed declaration, instead of two separate type checks.
The notes are shown only when a declaration link is shown, so a note never appears without its link.

Declined

DRY: declarationPositions and declarationNotes are declared on both RefinementErrorDTO and StateRefinementErrorDTO. This follows the existing declarationPosition. Moving them into LJErrorDTO would add them to every error type, most of which have no declaration.
declarationNotes ?? [] is kept as a guard, because lsp4j leaves out null fields.

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

Codex review, round 1

codex exec review --base origin/main:

[P1] Use a published verifier version (server/pom.xml). liquidjava-verifier:0.0.38 is not on Maven Central yet, so the server build fails.
[P2] Format declaration positions when copying diagnostics (diagnostics.ts). The copy button would paste the new declarationPositions as raw JSON.

Fixed

P2: formatDiagnosticForClipboard now skips declarationPositions, as it already skips declarationPosition. The copied text keeps Declaration Notes: where …. The location test now also checks the copied text.

Declined

P1: this is intended and stated in the PR body. The PR needs the 0.0.38 release with Show states of named sets by their set in state hints and declared-here liquidjava#517 and #525, and should not be merged before that release. I tested it locally against #525's head, installed as 0.0.38 in an isolated Maven repository.

Tests: 125 unit, typecheck, lint, and 39 server tests (against 0.0.38 from #525) pass.

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

Codex review, round 2

[P1] Publish the verifier version before depending on it (server/pom.xml). This is the same point as round 1.
[P2] Show declaration notes when no declaration link exists (sections.ts).

Declined (both)

P1: declined for the same reason as in round 1. The PR waits for the 0.0.38 release and says so in its body.
P2: the notes explain the declaration excerpt. The verifier prints them only under that excerpt (LJDiagnostic.toString() prints getDeclarationNotes() only after a declaration snippet). Without a declaration link, a line such as where closed(this) means … would point at nothing the user can see. The server test builds that combination only to check that the field is copied. It is not a case the verifier produces.

Codex found nothing else, so the loop ends here.

The server sends the verifier's declaration positions and declaration notes (the "where ... means ..." lines) of refinement and state errors, and the Locations section shows a link to every position, with the notes under them. Needs liquidjava-verifier 0.0.38: getDeclarationNotes() comes from liquid-java/liquidjava#517 and getDeclarationPositions() from liquid-java/liquidjava#525. 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>

…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

CatarinaGamboa mentioned this pull request Nov 10, 2026

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

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 2 commits November 11, 2026 14:22

Leave the declaration positions out of a copied error

43580f4

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

CatarinaGamboa force-pushed the feat/181-declaration-notes branch from d0a4a6e to 43580f4 Compare November 11, 2026 14:28

CatarinaGamboa merged commit 3a4d92f into main Nov 11, 2026
3 of 6 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

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

Show every declared-here position and its gloss in the IDE panel#191
CatarinaGamboa merged 2 commits into
mainfrom
feat/181-declaration-notes

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!

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

Verifier version: needs 0.0.38 (not yet released)

Before → after (Locations section, at the study width)

Overlap with open PRs

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!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading