From 8a2158f630a6fc46a56aa2eaad5d4e56256251ee Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 15:24:24 +0000 Subject: [PATCH 1/2] Show every declared-here position and its gloss in the IDE panel 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 --- client/src/types/diagnostics.ts | 8 ++++++++ client/src/webview/script.spec.ts | 2 +- client/src/webview/state-errors.spec.ts | 2 ++ client/src/webview/styles.ts | 6 ++++++ .../views/diagnostics/diagnostics.spec.ts | 19 ++++++++++++++++++- client/src/webview/views/sections.ts | 12 ++++++++---- server/pom.xml | 2 +- .../java/dtos/errors/RefinementErrorDTO.java | 8 ++++++++ .../dtos/errors/StateRefinementErrorDTO.java | 6 ++++++ .../java/utils/DiagnosticConverterTest.java | 8 ++++++-- 10 files changed, 64 insertions(+), 9 deletions(-) diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 36ab1c4..4bb81ce 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -73,6 +73,10 @@ export type RefinementError = BaseDiagnostic & { customMessage: string; counterexample: Counterexample; declarationPosition: SourcePosition | null; + // where each part of the refinement is declared, the first being declarationPosition + declarationPositions: SourcePosition[]; + // lines that explain the declaration, shown under its locations + declarationNotes: string[]; } export type Counterexample = { @@ -99,6 +103,10 @@ export type StateRefinementError = BaseDiagnostic & { found: VCSimplificationResult; customMessage: string; declarationPosition: SourcePosition | null; + // where each entry state that makes up expected is declared, the first being declarationPosition + declarationPositions: SourcePosition[]; + // lines that explain the declaration, shown under its locations + declarationNotes: string[]; // one state machine per state set of the receiver's class stateMachines: LJStateMachine[]; } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 270f4c3..70ac935 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -63,7 +63,7 @@ function stateError(title: string, sm: LJStateMachine, line = position.lineStart title, message: `${title} message`, hints: [], file, position: errorPosition, category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)', found: { implication: null as never, origin: null, simplification: 'Closed(counter)' }, - customMessage: '', declarationPosition: null, stateMachines: [sm], + customMessage: '', declarationPosition: null, declarationPositions: [], declarationNotes: [], stateMachines: [sm], }; } diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index 93ee165..51f1f50 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -26,6 +26,8 @@ function stateError(line: number, overrides: Partial = {}) found: { implication: null as never, origin: null, simplification: null }, customMessage: '', declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }, + declarationPositions: [{ file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }], + declarationNotes: [], stateMachines: [machine()], ...overrides, }; diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e682ed1..c3f0d68 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -377,6 +377,12 @@ export function getStyles(): string { .link:hover { text-decoration: underline; } + .location-note { + display: block; + padding-left: 2ch; + text-indent: -2ch; + color: var(--vscode-descriptionForeground); + } .lj-expression, .lj-expression-code { font-family: var(--vscode-editor-font-family); diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 8d9d430..848083a 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/client/src/webview/views/diagnostics/diagnostics.spec.ts @@ -1,5 +1,6 @@ import { afterEach, describe, expect, it } from 'vitest'; -import type { CustomError, CustomWarning } from '../../../types/diagnostics'; +import type { CustomError, CustomWarning, StateRefinementError } from '../../../types/diagnostics'; +import { renderLocation } from '../sections'; import { renderDiagnosticsView } from './diagnostics'; const currentFile = 'file:///workspace/Current.java'; @@ -86,6 +87,22 @@ describe('diagnostics view', () => { expect(document.querySelector('#show-all-button')).toBeNull(); }); + it('shows every declaration of a refinement with their notes under them', () => { + const declaredAt = (lineStart: number) => + ({ file: '/workspace/DoorRefinements.java', lineStart, colStart: 29, lineEnd: lineStart, colEnd: 58 }); + document.body.innerHTML = renderLocation({ + ...error(), type: 'state-refinement-error', declarationPosition: declaredAt(12), + declarationPositions: [declaredAt(12), declaredAt(13)], + declarationNotes: ['where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar'], + } as unknown as StateRefinementError); + + expect(Array.from(document.querySelectorAll('pre > *')).map(element => element.textContent)).toEqual([ + 'DoorRefinements.java:13', 'DoorRefinements.java:14', + 'where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar', + ]); + expect(document.querySelector('pre > :last-child')?.className).toBe('location-note'); + }); + it.each([false, true])('keeps warnings in the passed state (showAll=%s)', showAll => { document.body.innerHTML = renderDiagnosticsView([warning(), warning(otherFile)], showAll, currentFile); diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index c7f6666..7f2a986 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -86,15 +86,19 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { const positions: SourcePosition[] = []; if (diagnostic.position && diagnostic.file) positions.push(diagnostic.position); - const declarationPosition = diagnostic.type === 'refinement-error' || diagnostic.type === 'state-refinement-error' - ? diagnostic.declarationPosition + const declaration = diagnostic.type === 'refinement-error' || diagnostic.type === 'state-refinement-error' + ? diagnostic : null; - if (declarationPosition?.file) positions.push(declarationPosition); + const declarationPositions = declaration?.declarationPositions.filter(position => position.file) ?? []; + positions.push(...declarationPositions); if (positions.length === 0) return ""; const title = positions.length === 1 ? "Location" : "Locations"; const links = positions.map(renderLocationLink).join("\n"); - return renderCustomSection(title, /*html*/`
${links}
`); + // the notes explain the declarations, so they are shown only under their links + const notes = declarationPositions.length > 0 ? declaration?.declarationNotes ?? [] : []; + const noteLines = notes.map(note => `${escapeHtml(note)}`).join(""); + return renderCustomSection(title, /*html*/`
${links}${noteLines}
`); }; export function renderVariableHighlightButton(variable: LJVariable): string { diff --git a/server/pom.xml b/server/pom.xml index a1a6d6b..1b4eb13 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -167,7 +167,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.37 + 0.0.38 io.github.liquid-java diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java index 3e3c0cd..196e5b2 100644 --- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java @@ -1,5 +1,7 @@ package dtos.errors; +import java.util.List; + import dtos.diagnostics.CounterexampleDTO; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.VCSimplificationResultDTO; @@ -16,6 +18,10 @@ public class RefinementErrorDTO extends LJErrorDTO { public final String customMessage; public final CounterexampleDTO counterexample; public final SourcePositionDTO declarationPosition; + /** Where each part of the refinement is declared, the first being declarationPosition */ + public final List declarationPositions; + /** Lines that explain the declaration, such as what the states it names mean */ + public final List declarationNotes; public RefinementErrorDTO(RefinementError error) { super("refinement-error", error); @@ -24,6 +30,8 @@ public RefinementErrorDTO(RefinementError error) { this.customMessage = error.getCustomMessage(); this.counterexample = CounterexampleDTO.from(error.getCounterexample()); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); + this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList(); + this.declarationNotes = error.getDeclarationNotes(); } public static RefinementErrorDTO from(RefinementError error) { diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index e994a45..7a83166 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -27,6 +27,10 @@ public class StateRefinementErrorDTO extends LJErrorDTO { public final VCSimplificationResultDTO found; public final String customMessage; public final SourcePositionDTO declarationPosition; + /** Where each part of the refinement is declared, the first being declarationPosition */ + public final List declarationPositions; + /** Lines that explain the declaration, such as what the states it names mean */ + public final List declarationNotes; public final List stateMachines; public StateRefinementErrorDTO(StateRefinementError error) { @@ -35,6 +39,8 @@ public StateRefinementErrorDTO(StateRefinementError error) { this.found = VCSimplificationResultDTO.from(error.getFoundSimplification()); this.customMessage = error.getCustomMessage(); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); + this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList(); + this.declarationNotes = error.getDeclarationNotes(); this.stateMachines = declarationPosition == null || declarationPosition.file() == null ? List.of() : stateMachines(declarationPosition.file(), specFiles(), error.getContext()); } diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index 1e24658..cc0ff4c 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -159,6 +159,7 @@ void preservesRefinementDetailsAndSimplificationHistory() { assertEquals("true", dto.expected); assertEquals("expected true", dto.customMessage); assertEquals(dto.position, dto.declarationPosition); + assertEquals(List.of(dto.position), dto.declarationPositions); assertEquals("false", dto.found.implication().predicate()); assertEquals("constant folding", dto.found.simplification()); assertEquals("true", dto.found.origin().implication().predicate()); @@ -170,15 +171,18 @@ void preservesRefinementDetailsAndSimplificationHistory() { @Test void preservesStateRefinementDetailsWithoutDeclarationFile() { StateRefinementErrorDTO dto = (StateRefinementErrorDTO) DiagnosticConverter.convertToDTO( - new StateRefinementError(position, null, new Predicate(new LiteralBoolean(false)), + new StateRefinementError(position, List.of(), new Predicate(new LiteralBoolean(false)), new VCSimplificationResult(new VCImplication(new Predicate())), null, "expected closed", - List.of(), null, null, UnaryOperator.identity())); + List.of(), null, null, UnaryOperator.identity(), + List.of("where closed(this) means doorState(this) == closed"))); assertEquals("error", dto.category); assertEquals("state-refinement-error", dto.type); assertEquals("false", dto.expected); assertEquals("true", dto.found.implication().predicate()); assertEquals("expected closed", dto.customMessage); assertNull(dto.declarationPosition); + assertEquals(List.of(), dto.declarationPositions); + assertEquals(List.of("where closed(this) means doorState(this) == closed"), dto.declarationNotes); assertEquals(List.of(), dto.stateMachines); } From d0a4a6e14bdd29f0dd9ae16a724ef55280ffa559 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:05:04 +0000 Subject: [PATCH 2/2] Leave the declaration positions out of a copied error Co-Authored-By: Claude Opus 5.5 --- .../src/webview/views/diagnostics/diagnostics.spec.ts | 10 +++++++--- client/src/webview/views/diagnostics/diagnostics.ts | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 848083a..c2bcb7a 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/client/src/webview/views/diagnostics/diagnostics.spec.ts @@ -1,7 +1,7 @@ import { afterEach, describe, expect, it } from 'vitest'; import type { CustomError, CustomWarning, StateRefinementError } from '../../../types/diagnostics'; import { renderLocation } from '../sections'; -import { renderDiagnosticsView } from './diagnostics'; +import { formatDiagnosticForClipboard, renderDiagnosticsView } from './diagnostics'; const currentFile = 'file:///workspace/Current.java'; const otherFile = 'file:///workspace/Other.java'; @@ -90,17 +90,21 @@ describe('diagnostics view', () => { it('shows every declaration of a refinement with their notes under them', () => { const declaredAt = (lineStart: number) => ({ file: '/workspace/DoorRefinements.java', lineStart, colStart: 29, lineEnd: lineStart, colEnd: 58 }); - document.body.innerHTML = renderLocation({ + const stateError = { ...error(), type: 'state-refinement-error', declarationPosition: declaredAt(12), declarationPositions: [declaredAt(12), declaredAt(13)], declarationNotes: ['where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar'], - } as unknown as StateRefinementError); + } as unknown as StateRefinementError; + document.body.innerHTML = renderLocation(stateError); expect(Array.from(document.querySelectorAll('pre > *')).map(element => element.textContent)).toEqual([ 'DoorRefinements.java:13', 'DoorRefinements.java:14', 'where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar', ]); expect(document.querySelector('pre > :last-child')?.className).toBe('location-note'); + // the copied error keeps the notes but not the raw positions + expect(formatDiagnosticForClipboard(stateError)).toContain('Declaration Notes: where closed(this) means'); + expect(formatDiagnosticForClipboard(stateError)).not.toContain('Declaration Positions'); }); it.each([false, true])('keeps warnings in the passed state (showAll=%s)', showAll => { diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index 800e07f..5eb0f06 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -96,7 +96,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: } export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string { - const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'stateMachines']); + const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'declarationPositions', 'stateMachines']); const lines: string[] = []; Object.entries(diagnostic).forEach(([key, value]) => {