LSP code action document version

Stream: lean4

[Richard Copley]

Here's the core Lean 4 code that constructs a WorkspaceEdit (part of the language server's response to a textDocument/codeAction request from the editor to implement "Try this:" suggestions):

def ofTextEdit (uri : DocumentUri) (te : TextEdit) : WorkspaceEdit :=
  /- [note], there is a bug in vscode where not including the version will cause an error,
  even though the version field is not used to validate the change.

  References:
  - [a fix in the wild](https://github.com/stylelint/vscode-stylelint/pull/330/files).
    Note that the version field needs to be present, even if the value is `undefined`.
  - [angry comment](https://github.com/tsqllint/tsqllint-vscode-extension/blob/727026fce9f8c6a33d113373666d0776f8f6c23c/server/src/server.ts#L70)
  -/
  let doc := {uri, version? := some 0}
  ofTextDocumentEdit { textDocument := doc, edits := #[te]}

I'd like to replace it with this:

def ofTextEdit (doc : VersionedTextDocumentIdentifier) (te : TextEdit) : WorkspaceEdit :=
  ofTextDocumentEdit { textDocument := doc, edits := #[te]}

Here are all the changes that would be needed: in core[edit: updated] and in Std.

• I think the code is easier to understand, even without a comment
• It conforms to the LSP specification
• There is at least one LSP client which does validate the version number here, namely the Eglot client included in Emacs

I have a fork of lean4-mode which uses Eglot. It has a workaround for this issue. I discussed it with the author of Eglot and he encouraged me to raise it with the Lean 4 community.

[Richard Copley]

The lean4-mode/Eglot workaround also addresses an issue that affects VS Code. All the code edits generated by apply? and friends have the same title, "Apply 'Try this'", so they are indistinguishable in the menu. The official lean4-mode based on lsp-mode isn't affected. Here is a VS code screenshot.
image.png

[Eric Wieser]

It might be worth opening a PR for this (with links to this Zulip thread to avoid duplicating discussion) so that it doesn't get forgotten

[Richard Copley]

I won't forget :smile:. I don't want to rebase it onto origin/master, so I'll PR this if and when my existing PRs are accepted or rejected.
[Sorry, thinking of something else.]

[Richard Copley]

Thanks @Eric Wieser. In lean4? (There's also a patch for std4.) Will I get in trouble if I don't open an RFC issue first?

[Eric Wieser]

You certainly won't get into trouble for opening the std4 PR. I can't comment on the RFC process for lean4.

[Richard Copley]

Great! I opened a self-contained std4 PR, #306

[Scott Morrison]

Thanks @Richard Copley. Joe and Marc will make sure that the code ends up in the right places between Std and core.

[Alexandre Rademaker]

Hi @Richard Copley should you ask to add Lean in the list https://github.com/joaotavora/eglot#connecting-to-a-server?

[Richard Copley]

I don't think so. You get something with out-of-the-box Eglot in Lean 4 files, but I wouldn't like to spend much time there. But try it for yourself and see what you think, if you want.

[Marc Huisinga]

Richard Copley said:

Thanks Eric Wieser. In lean4? (There's also a patch for std4.) Will I get in trouble if I don't open an RFC issue first?

As discussed in the std4 issue, it's fine to open a core PR for the parts that belong in core without a corresponding RFC.

[Richard Copley]

Marc Huisinga said:

As discussed in the std4 issue, it's fine to open a core PR for the parts that belong in core without a corresponding RFC.

The sequencing is delicate. Ultimately I want to modify WorkspaceEdit.ofTextEdit in core, to take a VersionedTextDocumentIdentifier instead of a uri. This is a natural change there: it streamlines and simplifies. But it breaks Std and Mathlib. This sequence would work:

• Std merges [#306]
• Mathlib adopts the new Std functions WorkspaceEdit.ofVersionedTextEdit and EditableDocument.versionedIdentifier [*]
• Core modifies .ofTextEdit (which now has no uses in Std or Mathlib) and adds EditableDocument.versionedIdentifier [*]
• Mathlib switches back to using the core functions
• Std deletes the two new functions and uses the core versions

[*] One of these would need a different name

The alternative is to have three PRs (in core, std, mathlib) which all need to be merged at the same time.

[Marc Huisinga]

I believe the typical process for these kinds of breaking changes so far is that the PR to core is merged and the PR to the downstream project waits until the next release (right @Scott Morrison?).

[Richard Copley]

Marc Huisinga said:

As discussed in the std4 issue, it's fine to open a core PR for the parts that belong in core without a corresponding RFC.

#2721

[Scott Morrison]

Yes. We typically just do the three PRs simultaneously. If you add the blocked-by-core-release label on Mathlib, and the depends on core changes label on Std, it makes it easier to track.

[Scott Morrison]

Best also to ping me directly so I know about them. :-)

[Richard Copley]

Ok. I will re-use the existing Std PR #306. Will you send me an invitation for mathlib please?

[Richard Copley]

@Scott Morrison, @Marc Huisinga , @Mario Carneiro, I have updated (and squashed and rebased) std #306 to depend on core #2721. I don't think I have the permission to add the depends on core changes label.

The mathlib change is fairly tiny:

index 6925f79f2..5a68902c5 100644
--- a/Mathlib/Tactic/Widget/Calc.lean
+++ b/Mathlib/Tactic/Widget/Calc.lean
@@ -21,7 +21,7 @@ open Lean Server RequestM

 /-- Code action to create a `calc` tactic from the current goal. -/
 @[tactic_code_action calcTactic]
-def createCalc : TacticCodeAction := fun params _snap ctx _stack node => do
+def createCalc : TacticCodeAction := fun _ _snap ctx _stack node => do
   let .node (.ofTacticInfo info) _ := node | return #[]
   if info.goalsBefore.isEmpty then return #[]
   let eager := {
@@ -37,7 +37,7 @@ def createCalc : TacticCodeAction := fun params _snap ctx _stack node => do
       let goal := info.goalsBefore[0]!
       let goalFmt ← ctx.runMetaM {} <| goal.withContext do Meta.ppExpr (← goal.getType)
       return { eager with
-        edit? := some <|.ofTextEdit params.textDocument.uri
+        edit? := some <|.ofTextEdit doc.versionedIdentifier
           { range := ⟨tacPos, endPos⟩, newText := s!"calc {goalFmt} := by sorry" }
       }
   }]

[Scott Morrison]

@Richard Copley, if you'd like to test it in place, you can edit the lean-toolchain in the std PR to say

leanprover/lean4-pr-releases:pr-release-2721

Then CI will run against your update to Lean.

[Scott Morrison]

(Same applied if you want to make a Mathlib PR.)

[Scott Morrison]

The next release will be at the end of October.

[Richard Copley]

I can do that if you want, but I have built and tested Lean and run the steps of Std's CI, locally, so I'm satisfied both PRs will pass CI.

[Richard Copley]

@Scott Morrison, can you send me an invitation to the Mathlib github repo?

[Scott Morrison]

@Richard Copley, done!

[Richard Copley]

Scott Morrison said:

Richard Copley, if you'd like to test it in place, you can edit the lean-toolchain in the std PR to say

leanprover/lean4-pr-releases:pr-release-2721

Then CI will run against your update to Lean.

Done, but the CI is not running. I introduced and then resolved a merge conflict when I changed lean-toolchain. Maybe it needs a maintainer to remove the merge-conflict label? and the CI is passing.

[Richard Copley]

Scott Morrison said:

(Same applied if you want to make a Mathlib PR.)

Done, Mathlib #7812.

[Richard Copley]

For the Mathlib CI for #7812 to succeed on the #2721 toolchain, I would need to point its lakefile/manifest to the Std branch for #306, and rebase the Mathlib branch for #7812 onto any other Mathlib4 commits that are required by recent changes to core or Std. I think. Seems tricky! Is there a script to help?

@Scott Morrison, is there a Mathlib branch corresponding to Std #304, for example?

[Richard Copley]

Richard Copley said:

Scott Morrison, is there a Mathlib branch corresponding to Std #304, for example?

#7771, for reference

[Scott Morrison]

Sorry, this is a bit of a mess.

[Scott Morrison]

The nightly-testing branch is very often a good place to start from. I try to keep that building against the latest nightly release.

[Scott Morrison]

But if you use the automatically generated lean-pr-testing-2721 branch, it should already have been started from nightly-testing.

[Scott Morrison]

If there are Std bumps in flight then ... you have to bug me. :-)

[Richard Copley]

Scott Morrison said:

Sorry, this is a bit of a mess.

It has a certain terrible beauty. I hope I'm not making things more difficult.

Current state of my 3 PRs:
The 3 changes to be merged are single commits.

Core #2721

• CI OK

Std #306

• Has a "do not merge" commit, to use the 2721 toolchain
• CI OK

Mathlib #7812

• Branch and PR based on lean-pr-testing-2721
• Has a "do not merge" commit, to use the 306 branch
• CI failing in an unrelated area, but does build the changed file Mathlib\Tactic\Widget\Calc.lean

Is that good enough?

[Scott Morrison]

@Richard Copley, thank you for your patience with this. :-)

Unfortunately the #7812 PR CI failures do seem to be related, could you please check those again?

[Richard Copley]

Scott Morrison said:

Unfortunately the #7812 PR CI failures do seem to be related, could you please check those again?

Thanks for catching that! After I wrote that message, I did a sneaky rebase which I assumed would work. Unfortunately I forgot to run lake update. #7812 is now in the state that I meant it to be in. CI is queued and I'm away to bed. :fingers_crossed:

[Richard Copley]

Trying again, but with the #7812 branch and PR based on nightly-testing instead of lean-pr-testing-2721 (because I need the std#304 changes) .
I also reordered the commits on the std#306 and #7812 branches so that the commit to be merged is the tip.
#7812 CI queued :green_circle: , std#306 awaiting approval.

[Scott Morrison]

Thanks @Richard Copley, one final thing that would make this perfect: the Mathlib PR should use the branch lean-pr-testing-2721. Then when the Mathlib CI checks out, the Lean PR will automatically lose its breaks-mathlib label and gain a builds-mathlib label.

(Sorry none of this is documented properly: we're working on it!)

[Scott Morrison]

Unfortunately one can't change the base branch of a PR without closing and opening a new one, so for now I'm just going to reset lean-pr-testing-2721 to match your richard-copley/code-action-document-version

[Richard Copley]

Scott Morrison said:

Unfortunately one can't change the base branch of a PR without closing and opening a new one, so for now I'm just going to reset lean-pr-testing-2721 to match your richard-copley/code-action-document-version

I think you can ... just click Edit next to the PR title.

[Scott Morrison]

That lets you change what you are proposing merging into, but not from.

[Scott Morrison]

That is, I still want the PR to say it is merging into master.

[Scott Morrison]

But the branch name containing the changes needs to be lean-pr-testing-2721, so our automation knows to report back to lean#2721.

[Scott Morrison]

(We could definitely fix this by e.g. directly inspecting the lean-toolchain, but no one has had the time to set this up.)

[Richard Copley]

Right, I think I see. Do you want me to close the PR and open a new one, or not?

[Scott Morrison]

No, it's fine as is. Thank you for your patience. Our workflow for changes touching 3 repos at once still needs some work. :-)

[Kevin Buzzard]

Richard I know you are a relatively new user -- thanks so much for your patience here! This entire lean 4 thing is very bleeding edge and a lot of independent parts are moving very fast right now making things somewhat chaotic and exciting at the minute.

[Richard Copley]

@Scott Morrison, It looks like I missed another lake update. #7812's lake-manifest.json points at a commit in my std fork that has been garbage-collected. I won't touch anything for now. If you would like me to update #7812, to try to get its CI green again, please let me know.

[Scott Morrison]

I'm hoping we're good to go. I'll merge the Std and Mathlib PRs into the respective nightly-testing branches tonight, and let you know if I run into trouble.

[Wojciech Nawrocki]

Hi @Scott Morrison, how can I rerun the mathlib CI on a lean4 PR (specifically lean4#2964)? (Sorry if this isn't the right thread: there has been some related discussion here.) EDIT: I have a guess now: create a branch lean-pr-testing-2964 on mathlib, and builds on that will be written back into the core thread by the bot.

[Scott Morrison]

Yes!

[Scott Morrison]

That branch should be automatically created by the bot.

[Scott Morrison]

As it is a slightly older PR, I would recommend to rebase the Lean PR onto nightly-with-mathlib

[Wojciech Nawrocki]

Now I am really derailing this thread, but; what is the established practice for PRs that require a patch to mathlib4 to work? Should I push directly to lean-pr-testing-xyzw, or should I make a new branch and mention it in the original lean4 PR?

[Scott Morrison]

Please push directly to lean-pr-testing-NNNN. It doesn't hurt to message me anytime you're working on a PR that requires this.

[Scott Morrison]

My attempt at documenting our system is at https://leanprover-community.github.io/contribute/tags_and_branches.html. Please complain! :-)