fix: version numbers in code actions #306
fix: version numbers in code actions #306bustercopley wants to merge 2 commits intoleanprover-community:mainfrom bustercopley:code-action-document-version-selfcontained
Conversation
|
Fixed unused variable linter errors |
|
@bustercopley Thanks, I'll find the right reviewer for this so we can figure out if it should belong in std or core. |
|
Thanks! |
|
From my reading of the spec, providing a null version means that the server has not yet heard of the file being open, rather than that the server simply doesn't want to send it, so this seems to strictly increase the conformance to the protocol. |
Std/CodeAction/Basic.lean
Outdated
|
|
||
| namespace Lean.Lsp.WorkspaceEdit | ||
|
|
||
| /-- Construct a WorkspaceEdit from a VersionedTextDocumentIdentifier and a TextEdit --/ |
There was a problem hiding this comment.
This should be in Std.Lean, maybe Std.Lean.Lsp, ditto for textDocument
There was a problem hiding this comment.
I think it may be better off in core as originally suggested by @bustercopley. Alternatively, if we keep it in std, we should delete ofTextEdit in core so that downstream users do not accidentally use the wrong function. I think I would personally prefer the former.
There was a problem hiding this comment.
Yes, especially since the changes to core amount to a simplificiation/streamlining, that is the natural place to do it. (I'm a bit intimidated by the process for core Lean PRs.)
There was a problem hiding this comment.
Yes, especially since the changes to core amount to a simplificiation/streamlining, that is the natural place to do it. (I'm a bit intimidated by the process for core Lean PRs.)
It's fine to PR this without a corresponding RFC since it is very small, uncontroversial and you discussed it with the Lean community and the respective code owner :)
There was a problem hiding this comment.
@mhuisi :) Do you mind saying something along those lines in the Zulip topic?
|
Force push: now depends on core #2721; squashed and rebased. |
Zulip topic
VS Code ignores the version number in a WorkspaceEdit but does not allow it to be null. There is at least one LSP client which does validate the version number, namely the Eglot client included in Emacs. By sending the correct version, we can be compatible with both.
This is a self-contained (std4-only) version, instead of the two changes (to lean4 and std4) that I mentioned on Zulip.