What to specify for `addSuggestion`

Stream: metaprogramming / tactics

[Gareth Ma]

Hi, I have this trivial tactic:

import Mathlib.Tactic.Basic

open Lean Elab.Tactic Std.Tactic.TryThis

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

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

def f := fun x ↦ x + 1
example : f 3 = 4 := by -- unsolved goals  ⊢ f 3 = 4
  change' a b c d e -- Try this: change f 3 = 4

Currently, it underlines the entire change' a b c d e part with green. However, when I use "try this", instead of the intended behaviour change f 3 = 4 appearing, I instead get change f 3 = 4 a b c d e, meaning it's only replacing change'.

I guess it's because [$sop:term]? is optional? But I don't know how to fix it.

[Gareth Ma]

Sorry if this is mentioned somewhere, I am new to metaprogramming and still slowly working through the book

[Gareth Ma]

Also according to the docs of [Std.Tactic.TryThis.]addSuggestion, it says if origSpan? is not provided, then the actual text to be replaced by suggestion will default to ref i.e. the part that's highlighted, and I am not sure why that' snot happening

[Mario Carneiro]

It works for me

[Gareth Ma]

It replaces correctly?

[Mario Carneiro]

yes, both the code action and the button replace the whole line

[Gareth Ma]

Okay it might be something to do with the Vim plugin I am using instead. Sorry for that!

[Mario Carneiro]

(actually not the whole line, the comment after the tactic is not deleted)

[Gareth Ma]

Yea but I think that's not part of the getRef

[Mario Carneiro]

it is

[Mario Carneiro]

but the code is smart about trailing whitespace

[Mario Carneiro]

there is also an option to adjust the hover to only cover change' (while still replacing the whole line), basically the opposite of what you are observing

[Gareth Ma]

elab_rules : tactic
| `(tactic|change'%$tx $[$sop:term]?) => withMainContext do
  let dstx ← delabToRefinableSyntax (←getMainTarget)
  addSuggestion tx (← `(tactic| change $dstx)) (extraMsg := "asdf")

I think for that, something like this works? (I copied the tactic change? in Mathlib)

[Mario Carneiro]

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

[Gareth Ma]

Oh nice, exactly the same :D

[Mario Carneiro]

without the origSpan?, it will have the issue you are reporting

[Gareth Ma]

I see, thanks a lot

[Julian Berman]

The VSCode plugin uses some tricky heuristics to get all of this correct. I don't really want to focus on reproducing it, what lean.nvim does to approximate is complicated enough -- I'd rather wait and hope someone improves things on the pure-Lean side :)

[Gareth Ma]

Uhhh I think there is a better way? The diagnostics objects already include end_lnum and end_col, but it seems both your code and VSCode doesn't use it...
I will make a PR uh soon
Screenshot-2023-10-19-at-21.42.02.png

[Julian Berman]

IIRC that doesn't properly handle stuff like trimming unnecessarily entering tactic mode, and also I think the ranges are wrong for some zero-length diagnostics, but it's been awhile since I've looked and I might be misremembering / it may have been fixed. As I say if you PR something happy to merge it if it passes all the tests and some new one, but otherwise I'm waiting for code actions :)

[Mario Carneiro]

I'm confused. The lean code specifies exactly how this is supposed to be handled, none of the work is in the extension

[Gareth Ma]

He is referring to the code here which handles replacing suggestions heuristically.