Skip to content

fix: guard LSP refresh requests behind capability check#12735

Open
wvhulle wants to merge 1 commit intoleanprover:masterfrom
wvhulle:wvhulle/lsp-refresh-guard
Open

fix: guard LSP refresh requests behind capability check#12735
wvhulle wants to merge 1 commit intoleanprover:masterfrom
wvhulle:wvhulle/lsp-refresh-guard

Conversation

@wvhulle
Copy link

@wvhulle wvhulle commented Feb 28, 2026

This PR fixes repeated spamming of LSP clients with responses the client never advertised in its set of capabilities.

May close: #7488

This PR guards diagnostic refresh requests behind capability checking so
editors that don't advertise refresh support don't receive unsolicited
requests.
@wvhulle wvhulle marked this pull request as ready for review February 28, 2026 12:05
@wvhulle wvhulle requested a review from mhuisi as a code owner February 28, 2026 12:05
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 28, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-28 12:43:56)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-28 12:43:57)

@wvhulle
Copy link
Author

wvhulle commented Mar 1, 2026

@wkrozowski I rebased on latest master but the bot still shows the message. Why is that?

@wvhulle wvhulle changed the title fix: guard LSP refresh requests behind capability check guard LSP refresh requests behind capability check Mar 1, 2026
@wkrozowski wkrozowski changed the title guard LSP refresh requests behind capability check fix: guard LSP refresh requests behind capability check Mar 1, 2026
@wkrozowski wkrozowski added changelog-server Language server, widgets, and IDE extensions changelog-no Do not include this PR in the release changelog and removed changelog-server Language server, widgets, and IDE extensions changelog-no Do not include this PR in the release changelog labels Mar 1, 2026
@wkrozowski
Copy link
Contributor

@mhuisi Marc, could you have a look at this PR?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

lsp: workspace/inlayHint/refresh

3 participants