feat: 'unsolved goals' & 'goals accomplished' diagnostics by mhuisi · Pull Request #7366 · leanprover/lean4

mhuisi · 2025-03-06T14:47:28Z

This PR adds server-side support for dedicated 'unsolved goals' and 'goals accomplished' diagnostics that will have special support in the Lean 4 VS Code extension. The special 'unsolved goals' diagnostic is adapted from the 'unsolved goals' error diagnostic, while the 'goals accomplished' diagnostic is issued when a theorem or Prop-typed example has no errors or sorrys. The Lean 4 VS Code extension companion PR is at leanprover/vscode-lean4#585.

Specifically, this PR extends the diagnostics served by the language server with the following fields:

leanTags: Custom tags that denote the kind of diagnostic that is being served. As opposed to the code, leanTags should never be displayed in the UI. Examples introduced by this PR are a tag to distinguish 'unsolved goals' errors from other diagnostics, as well as a tag to distinguish the new 'goals accomplished' diagnostic from other diagnostics.
isSilent: Whether a diagnostic should not be displayed as a regular diagnostic in the editor. In VS Code, this means that the diagnostic is displayed in the InfoView under 'Messages', but that it will not be displayed under 'All Messages' and that it will also not be displayed with a squiggly line.

The isSilent field is also implemented for Message so that silent diagnostics can be logged in the elaborator. All code paths except for the language server that display diagnostics to users are adjusted to filter Messages with isSilent := true.

ghost · 2025-03-06T16:05:33Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-7366 has successfully built against this PR. (2025-03-06 16:05:32) View Log
✅ Mathlib branch lean-pr-testing-7366 has successfully built against this PR. (2025-03-06 17:05:35) View Log
✅ Mathlib branch lean-pr-testing-7366 has successfully built against this PR. (2025-03-07 10:35:51) View Log
✅ Mathlib branch lean-pr-testing-7366 has successfully built against this PR. (2025-03-07 11:41:06) View Log
✅ Mathlib branch lean-pr-testing-7366 has successfully built against this PR. (2025-03-07 14:34:56) View Log

tydeu

LGTM! I only have a minor style suggestion.

Vtec234 · 2025-03-06T22:44:29Z

Will an off-the-shelf LSP client without special support for Lean ignore silent diagnostics, i.e., not show them as squiggles? The vscode-lean4 diff in which you explicitly filter them makes me think they would not be ignored which is not great for editors other than VSc.

mhuisi · 2025-03-07T08:17:12Z

Will an off-the-shelf LSP client without special support for Lean ignore silent diagnostics, i.e., not show them as squiggles? The vscode-lean4 diff in which you explicitly filter them makes me think they would not be ignored which is not great for editors other than VSc.

No, they won't, similar to how our handling of diagnostic ranges will already result in a bad editing experience for clients that do not support fullRange. Fortunately, most LSP clients also support some sort of middleware that Lean plugins can use to implement support for silent diagnostics. NeoVim support for silent diagnostics is upcoming.

I considered turning all silent diagnostics into "hint" severity diagnostics, but it doesn't look like LSP clients render those without a squiggly consistently across the board, either, so I think I would prefer to retain the severity axis for silent diagnostics.

I also considered implementing an entirely separate notification for this that is identical to publishDiagnostics, except that all diagnostics served by it are silent, but concluded that it would simply be too annoying for clients to have to synchronize these two separate notifications whenever they need to funnel them into a shared UI, like 'Messages'.
Essentially, we would need something like an additional version field on both diagnostic notifications for this that allows versioning the messages in the stream of diagnostics we serve for each elaboration run of a document version, so that clients can then use this version to implement a consistent non-racey merge logic. Alternatively, they could also rely on language server internals like how and in which order these notifications are served, which is not great either. I much prefer the isSilent field over both of these approaches.

Two other ideas by @Kha are to have the silent diagnostics in a separate field in the publishDiagnostics notification so that they are synchronized by default, or to introduce a client capability for silent diagnostics. I think the last option might be the best one of these, if only to not display the squigglies for users who are stuck on an old vscode-lean4 version for some reason.

mhuisi · 2025-03-07T12:27:38Z

@Vtec234 We now define a client capability for silent diagnostics and filter silent diagnostics from the server if the capability isn't set.

This PR adds several new editor decorations. ### Error and warning gutter decorations To resolve the issue that warnings and errors can sometimes be a bit difficult to spot, especially when the corresponding diagnostic squiggly is small, this PR adds a system of gutter decorations to make errors and warnings much more visible. ![Error and warning gutter decorations](https://github.com/user-attachments/assets/a611e2ea-aa26-4c1f-b945-8e86dfbeef4c) The circled error and warning symbols denote the line where an error or a warning starts, i.e. where the squiggly is displayed. A red vertical line denotes the *full range* of the error, i.e. the range in which the error is displayed under 'Messages' in the InfoView. The red line bends to the right whenever a full error range ends in that line of code. Single line errors are displayed without a red line. These gutter decorations can be disabled using the 'Lean4: Show Diagnostic Gutter Decorations' setting. When the gutter icons of the Error Lens extension are enabled, the gutter decorations of the Lean 4 VS Code extension are disabled. Once this PR is merged, this feature will be available in all Lean 4 versions. ### 'Unsolved goals' markers To resolve the issue that it can sometimes be a bit difficult to tell where one should continue typing in a proof, this PR adds an end-of-line editor decoration that is displayed in the line where the full range of an 'unsolved goals' error ends. ![Unsolved goals markers](https://github.com/user-attachments/assets/32562122-6ce6-490e-a9db-5ae3e8a6e79f) The 'unsolved goals' markers can be disabled using the 'Lean 4: Show Unsolved Goal Decoration' setting. This feature needs language server support, so it will only be active for Lean versions that include the companion PR at leanprover/lean4#7366. ### Goals accomplished! To re-introduce some positive reinforcement into Lean 4 after the 'Goals accomplished!' message from Lean 3 was removed due to often being confusing in Lean 4, this PR adds a new 'Goals accomplished!' mechanism when a theorem or a `Prop`-typed `example` has been proven. ![Goals accomplished](https://github.com/user-attachments/assets/f303d580-cd4a-4697-80e6-d0d1114fd454) When a theorem or a `Prop`-typed `example` contains no errors or `sorry`s anymore, two blue checkmarks appear next to the start of the declaration as a gutter decoration. Additionally, a 'Goals accomplished!' message appears under 'Messages' in the InfoView. The 'Goals accomplished!' message does not appear in 'All Messages' and is not displayed with a squiggly line in the editor. The 'Goals accomplished!' gutter decoration can be configured or disabled using the 'Lean 4: Goals Accomplished Decoration Kind' setting. In addition to the default double checkmark decoration pictured above, this PR adds the following additional styles for the gutter decoration: - Circled checkmark: ![Circled checkmark](https://github.com/user-attachments/assets/0014bf2c-6dee-4af7-9c01-7cd470efa1ca) - Octopus: ![Octopus](https://github.com/user-attachments/assets/9a65ad3b-d032-414c-b632-3afc943d45ae) - Tada: ![Tada](https://github.com/user-attachments/assets/942e3973-444c-4701-b86a-0570ff437cd0) This feature needs language server support, so it will only be active for Lean versions that include the companion PR at leanprover/lean4#7366. ### Technical notes - We intend to test this implementation for the 'unsolved goals' markers and 'Goals accomplished!' in core before v4.19.0-rc1 to iron out any remaining issues. - All gutter decorations are implemented using .svgs, which is the only API that VS Code provides to display things in the gutter. Since there are lots of different cases to consider for the red vertical error range lines, as well as for light and dark themes, this PR ships 56 .svg files in total. - The design language of the red lines for the error range gutter decorations is deliberately not perfectly unambiguous. For example, when multiple full error ranges overlap, it isn't clear which error range is terminated by the line bending to the right. The design in this PR is the best I could come up with for the limited size of the gutter without introducing too much visual complexity or noise. - The task gutter had to be rewritten entirely for this PR, including the progress bar code. - Since the line where the full range of an 'unsolved goals' error ends is relatively unstable as the document is being edited, this PR implements an edit delay of 3000ms for 'unsolved goals' markers, so that they do not constantly jump around while editing the document. - The 'unsolved goals' markers use an emoji (specifically the 'Hammer and wrench' emoji U+1F6E0) instead of an icon. The reason for this is that VS Code's decoration API appears to be pretty broken for end-of-line icons and fails to vertically center them correctly. - None of these decorations have an associated hover to explain the semantics of each decoration. The reason for this is that VS Code doesn't support gutter decoration hovers and for end-of-line decorations, it pollutes the hover of every hover in the whole line with the hover message of the end-of-line decoration. - This PR includes the client-side for the protocol extensions defined at leanprover/lean4#7366.

Kha · 2025-03-08T09:23:32Z

Speedcenter results are concerning: https://speed.lean-lang.org/lean4/run-detail/70829899-6d71-46c7-a58c-039cb3bd0671

This PR addresses a performance regression noticed at #7366 (comment). It also ensures that we also consider the current message log when logging the goals accomplished message. `Language.Lean.internal.cmdlineSnapshots` in `Lean.Language.Lean` is moved to `Lean.internal.cmdlineSnapshots` in `Lean.CoreM` to make the option available in the elaborator.

There's still a bit more we can replicate from the below-referenced PR, but this essentially: * does not show virtual text or underlines for Lean's new `isSilent` diagnostics (in particular for goals accomplisehd ones) * puts them in a separate Neovim diagnostic namespace so they are still available * adds support for unsolved goal markers via an `extmark`, shown at end of line More configurability is also likely to be useful before advertising this but I want to test it out for a bit. Refs: leanprover/lean4#7366 Refs: leanprover/vscode-lean4#585

In other words, fold the (new isSilent) Goals Accomplished diagnostic into our existing logic for counting current goals. This behavior now differs from VSCode (which will show two messages in this case, one saying `No goals.` at the top and a second diagnostic saying `Goals accomplished` in Messages). In older Lean versions where we do not have the language server telling us whether goals are accomplished or not, we fall back (via `lean_no_goals_message`) such that we preserve our old behavior. We do this by comparing against the Lean *language server version* (sent in the `initialize` response, and which will be <0.3.0 for older Lean). Refs: leanprover/lean4#7624 Refs: leanprover/lean4#7366

mhuisi added 2 commits March 6, 2025 15:24

feat: 'unsolved goals' & 'goals accomplished" diagnostics

c42db0b

test: adjust interactive tests

1e16bc0

mhuisi added the changelog-server Language server, widgets, and IDE extensions label Mar 6, 2025

mhuisi requested review from Kha, Vtec234, digama0 and tydeu as code owners March 6, 2025 14:47

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 6, 2025

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025

Update lean-toolchain for testing leanprover/lean4#7366

9fe0011

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025

Update lean-toolchain for testing leanprover/lean4#7366

59f81e6

feat: issue 'goals accomplished' on non-sorry warnings

1835036

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025

Trigger CI for leanprover/lean4#7366

081b174

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025

Trigger CI for leanprover/lean4#7366

5c696d4

ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 6, 2025

This was referenced Mar 6, 2025

feat: editor decorations leanprover/vscode-lean4#585

Merged

RFC: No goals should point to errors elsewhere #4190

Closed

tydeu approved these changes Mar 6, 2025

View reviewed changes

Comment thread src/lake/Lake/Build/Actions.lean Outdated

Comment thread src/Lean/Language/Basic.lean Outdated

refactor: lake review comments

cb08d1e

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

f4d9a1e

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

9188e52

Kha approved these changes Mar 7, 2025

View reviewed changes

Comment thread src/Lean/Elab/MutualDef.lean

Comment thread src/Lean/Language/Util.lean Outdated

Comment thread src/Lean/Message.lean

Comment thread src/Lean/Elab/MutualDef.lean

chore: address elab & language processor review comments

ca890f1

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

ca02465

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

bcc0134

feat: client capability for protocol extensions

3dd2dc4

test: adjust test

d7dd892

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

5be95f1

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

d1a24aa

fix: wait for kernel task and use sorry message

0197d71

Kha approved these changes Mar 7, 2025

View reviewed changes

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

a146885

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025

Trigger CI for leanprover/lean4#7366

5aedef1

mhuisi added this pull request to the merge queue Mar 7, 2025

Merged via the queue into leanprover:master with commit dc5eb40 Mar 7, 2025
15 checks passed

mhuisi mentioned this pull request Mar 10, 2025

fix: only log goals accomplished in language server #7416

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: 'unsolved goals' & 'goals accomplished' diagnostics#7366

feat: 'unsolved goals' & 'goals accomplished' diagnostics#7366
mhuisi merged 8 commits intoleanprover:masterfrom
mhuisi:mhuisi/goal-markers

mhuisi commented Mar 6, 2025 •

edited

Loading

Uh oh!

ghost commented Mar 6, 2025 •

edited by ghost

Loading

Uh oh!

tydeu left a comment

Uh oh!

Uh oh!

Uh oh!

Vtec234 commented Mar 6, 2025 •

edited

Loading

Uh oh!

mhuisi commented Mar 7, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mhuisi commented Mar 7, 2025

Uh oh!

Uh oh!

Kha commented Mar 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

mhuisi commented Mar 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Mar 6, 2025 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tydeu left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Vtec234 commented Mar 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mhuisi commented Mar 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mhuisi commented Mar 7, 2025

Uh oh!

Uh oh!

Kha commented Mar 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mhuisi commented Mar 6, 2025 •

edited

Loading

ghost commented Mar 6, 2025 •

edited by ghost

Loading

Vtec234 commented Mar 6, 2025 •

edited

Loading

mhuisi commented Mar 7, 2025 •

edited

Loading