TryThis text for deletions

Stream: lean4

[Vlad Tsyrklevich]

I want to add a code suggestion to delete a block of text, but currently the link the TryThis tactic suggests has the link text as the replacement text, so if your suggestion is "" to just delete text you can't click on anything. I'd like to update TryThis to handle this case properly--the UI change I can imagine is either 1) if the suggestion text is blank, display the suggestion as "(delete text)" or 2) make the "Try this: " header text be a link if the suggestion text is empty, and then the caller can change the message to be something custom like "Delete this". Both seem fine to me, does anyone have an opinion before I make this change and PR it?

#mwe for those curious

import Lean

open Lean Elab Command Term Meta

syntax (name := test) (priority := default + 3) declModifiers
  group(("lemma" <|> "theorem") declId ppIndent(declSig) declVal) : command

@[command_elab test]
def testtest : CommandElab := fun stx => do
  let matchNodeName (n : Name) : Syntax → Bool
    | Syntax.node _ kind _ => kind == n
    | _ => false
  let some declId := stx.find? (matchNodeName `Lean.Parser.Command.declId) | throwError "err"

  let suggestion : Lean.Meta.Tactic.TryThis.Suggestion :=
    { suggestion := s!"" --- Blank suggestion text causing the issue
      toCodeActionTitle? := .some (fun _ => "toCodeActionTitle? text")}
  liftTermElabM <| Lean.Meta.Tactic.TryThis.addSuggestion declId suggestion (header := "header text: ")

theorem mythm : False := sorry

[Joachim Breitner]

There is a third option: Extend the API to give control over the text of the try-this link. This is also needed with very large try-this code actions. (This is the “alternative text” part of https://github.com/leanprover/lean4/issues/4551)

According to https://github.com/leanprover/lean4/issues/4551#issuecomment-2212462024 for mathlib you can use https://leanprover-community.github.io/mathlib4_docs/ProofWidgets/Component/MakeEditLink.html#ProofWidgets.MakeEditLink instead of TryThis with more flexibility.

Also relevant maybe: https://github.com/leanprover/lean4/issues/2064

[Vlad Tsyrklevich]

Thanks for the links!

[Vlad Tsyrklevich]

Another thing I find myself wanting to do: Don't just make a user-facing suggestion, but also make the actual edit on disk. In normal cases obviously this is not desirable, but if I'm writing a linter with lots of suggestions, this is easier than trying to do it in the IDE or writing a script to make the edits since every change may cause other downstream changes that you then also want to apply, without iteratively re-building mathlib mutliple times

[Vlad Tsyrklevich]

This seems to be supported in theory via LSP CodeActions: docs#Lean.Lsp.WorkspaceEdit I just don't see it implemented anywhere yet, corrections welcome!

[Vlad Tsyrklevich]

I guess one problem is that since you're editing a file as it's being compiled, this may require some deep compiler/lake integration to work the way you expect it to, depending on your use case.

[Thomas Murrills]

Re: TryThis suggestions for deletion, specifically: I think it would be intuitive for the suggestion in the infoview to repeat the source text but styled as red and struck-through, so that you can see what is being deleted as you click on it, without having to look somewhere else.

This still requires changing the behavior of TryThis to not display an empty string; I fully support any attempt to make TryThis much more flexible! :) Some infoview improvements have landed since the API was designed, and it's probably time for an overhaul.

I also think it makes sense to have both control over the suggestion text and sensible behavior when suggesting "" to avoid putting needless responsibility on the caller of TryThis.