"Try this" replaces incorrect segment

[grhkm21]

Hi. Here's code:

import Mathlib.Tactic.Basic

open Lean Elab.Tactic Std.Tactic.TryThis

syntax (name := change') "change'" (ppSpace colGt term)? : tactic

elab_rules : tactic
| `(tactic|change'%$tk $[$sop:term]?) => withMainContext do
  let dstx ← delabToRefinableSyntax (← getMainTarget)
  addSuggestion tk (← `(tactic| change $dstx)) (origSpan? := ← getRef)

def f := fun x ↦ x + 1
def g := fun x ↦ x + 1
example : f 3 = 4 := by
  change' a b c d e f g

With this code, it is supposed to change the entire line, as specified by origSpan?. Apparently it does on VSCode c.f. Mario. However, the plugin doesn't - it replaces it with f 3 = 4 a b c d e f g.

[Julian]

This seems to work correctly here (now?). I'm on Lean 4.3.0rc1, Mathlib4 df32aa2ebe0f1ef9bce7831b1bcc0723f07a4724 and NVIM v0.9.4. Can you confirm whether it does or doesn't for you?

[grhkm21]

Hi, sorry for the late reply. No, it doesn't work for me. I'm on NVIM v0.9.4, Lean v4.3.0-rc1, Mathlib b6ec7450650a5945bf4244751be4a5cf1fee962f. It's very interesting that it works for you, my understanding is it shouldn't...

Also, I think I have a fix idea, but I haven't gotten to implement it yet. Essentially, we should implement the .getWidgets RPC (found here) and use those directly to get the replacement range (and the js widget source code, which we ignore for now).

[Julian]

This is what I see here:

Screen.Recording.2023-11-06.at.10.34.05.PM.mov

Will need some way of reproducing the broken behavior I think

[Julian]

To be sure -- are you using lean.trythis.swap or the code action here? You should be using the latter on Lean 4, given it exists now.

[grhkm21]

I was using trythis, and I have gotten it to work with code action now :) Thanks a lot!

[Julian]

Cool, ok glad it works, I'll try to make this clearer -- I'd already removed lean.trythis from the readme but I think the next step would be not binding it at all in Lean 4 buffers, which should send a message at least. I'll likely do that and then close this. Thanks regardless for the issue.