Copying from the widget view

Stream: lean4

[Eric Wieser]

A pretty common workflow for me is:

• dsimp
• Copy the goal
• change $clipboard

Copying from the goal view is rather frustrating though; the clipboard symbol that was present in the Lean3 info view appears to have disappeared. Is there an existing feature to copy a subexpresion from the info view that I'm just missing?

[Eric Wieser]

Often what happens is instead dsimp ends up in my clipboard

[Damiano Testa]

Would a Try this tactic that suggests the pp goal be good enough?

[Damiano Testa]

Also, I do get the clipboard icon sometimes, specifically on the output of logInfo.

[Damiano Testa]

For instance, with this:

import Mathlib.Tactic

open Lean Elab Tactic in
elab "cg" : tactic => do logInfo m!"change {← getMainTarget}"

example : True := by
  cg  -- change True

if I leave the cursor on cg, then I can copy from the infoview clipboard change True and paste it.

[Damiano Testa]

It would probably be easy to make cg take a term (with metavariables) as input, scan the target and print out a match of that, rather than the whole goal.

[Damiano Testa]

Here is an example possibly closer to what you said:

example : (fun x : ℕ => x) 0 = 1 := by
  dsimp
  cg  -- change 0 = 1

[Eric Wieser]

Ah, I guess this is an obvious candidate for a change? _

[Damiano Testa]

Ok, I can try to get the Try this working, but I won't have time for a little bit. After that, I imagine that also a change? at ... will be next, right?

[Damiano Testa]

Btw, the _ in change? _ is superfluous, right?

[Eric Wieser]

No, because I want it to work for change? foo _and tell me the resulting _, even if foo was not in the goal

[Mario Carneiro]

let's say it's optional

[Eric Wieser]

Should change? run dsimp, or is that better as change!?

[Damiano Testa]

Ah, ok. I like the optional bit, but I had not understood the other one. _ was a place-holder for any term, not just a metavariable!

[Mario Carneiro]

no, that should be spelled dsimp; change?

[Mario Carneiro]

and then delete the dsimp

[Eric Wieser]

That has the annoying outcome that the try this doesn't delete the dsimp automatically

[Damiano Testa]

or dchange??

[Eric Wieser]

Could dsimp? suggest two try-this actions?

[Mario Carneiro]

there are lots of things you might want to run, seems better not to get too fancy

[Eric Wieser]

One that's dsimp only [...], and one that's change ...?

[Mario Carneiro]

I would probably suggest it as a code action but not a try this specifically

[Damiano Testa]

Anyway, I see that there is Lean.Expr.find?, but it takes a Expr -> Bool argument. Is there an Expr.findM? for monadic search?

[Mario Carneiro]

what are you looking for?

[Damiano Testa]

(I would run this on isDefEq (the given term) (the actual target).

[Mario Carneiro]

why find? then?

[Mario Carneiro]

this should just be one isDefEq call

[Damiano Testa]

To replace the _ with what it finds on the target expression. Maybe I minsunderstood the meaning of change? foo _.

[Damiano Testa]

Ah, but would that not then replace, possibly, the given foo?

[Mario Carneiro]

• elaborate foo _ to get a term t
• unify t with the goal
• instantiateMVars in t
• pretty print it

[Damiano Testa]

Ok, does this guarantee that foo will show up in the pp output?

[Mario Carneiro]

it will, unless foo is a parser-only syntax

[Damiano Testa]

Ok, then yes, I understand.

[Eric Wieser]

Oh, I was envisaging the dumber approach of "run change $arg, replace it with change $(currentGoal)"

[Damiano Testa]

Here is a possible tactic:

import Mathlib.Tactic

syntax "change?" (ppSpace colGt term)? : tactic

open Lean Meta Elab Tactic in
elab_rules : tactic
| `(tactic| change? $[$h]?) => do
  let expr := ← match h with
    | none => getMainTarget
    | some ex => do
      let ex := ← elabTerm ex none
      let defeq? := ← isDefEq ex (← getMainTarget)
      if ! defeq? then throwError "The given term is not DefEq to the goal"
      instantiateMVars ex
  logInfo m!"change {expr}"

example : (fun x : ℕ => x) 0 = 1 := by
  dsimp
  change? _ = 1  -- change 0 = 1
  change?        -- change 0 = 1
  change? _      -- change 0 = 1
  change? 1 = _  -- The given term is not DefEq to the goal

[Damiano Testa]

#6471

[Damiano Testa]

I am trying to implement the Try this feature. I got it almost working. What I am missing is that I would like to replace the whole tactic with the suggestion and I am unable to give a name to the right syntax. Here is what I have:

syntax "change?" (ppSpace colGt term)? : tactic

open Lean Meta Elab.Tactic Std.Tactic.TryThis in
elab_rules : tactic
| `(tactic| change?%$tk $[$h]?) => do   -- <-- I'd like `tk` to encompass everything, from `change?` until the end of the tactic
  [stuff]
  addSuggestion tk (← `(tactic| change $stx))

I would be happy also with replacing only the input starting from the question mark forwards (and then not printing change in the output).

[Wojciech Nawrocki]

Is there an existing feature to copy a subexpresion from the info view that I'm just missing?

Would it help if the right-click context menu actually worked, i.e. you could right-click a subexpression that gets highlighted and copy it from there?

[Wojciech Nawrocki]

Quick demo: out.mp4

[Kevin Buzzard]

That would be a great improvement!

[Eric Wieser]

Yes, that's the feature that I think I actually wanted!

[Wojciech Nawrocki]

Well, it's already in vscode-lean4 (new release) :)

[Mac Malone]

@Wojciech Nawrocki Another neat nice-to-have would be for go-to-def etc to be in the context menu as well (so one does not have to remember the keyboard shortcut).

[Wojciech Nawrocki]

That's annoying difficult to do afaict. At least in VSCode, the context menu is controlled by VSCode itself and you get very limited options for what actions it can take. We may have to reimplement all context menu functionality in JS to do that. (Don't want to discourage anyone from trying though, there may be a way!)

[Filippo A. E. Nuccio]

Wojciech Nawrocki said:

Well, it's already in vscode-lean4 (new release) :smile:

@Wojciech Nawrocki I have the latest version of vscode-lean4 but this features still does not work for me (Win11). Is it normal?

[Eric Wieser]

I still find copying from the infoview unreliable, even if I use that context menu

[Eric Wieser]

I constantly end up with the current tactic in my clipboard instea

[Patrick Massot]

Same here, but it really seems VSCode is broken, it has nothing to do with the infoview.

[Shreyas Srinivas]

I was able to implement a copy operation that works reliably using the vscode api. I am sure the clipboard api works. The place to look for might be the selection api.

[Wojciech Nawrocki]

Hm, unfortunately I don't have a Windows machine to test on. It works for me on macOS.

[Scott Morrison]

On macOS, I very often fail to copy and paste sub-expressions from the info view successfully. I can select, but then either cmd-c does nothing, or right clicking to get the context menu results in the selection changing.

[Filippo A. E. Nuccio]

Same here...

[Wojciech Nawrocki]

right clicking to get the context menu results in the selection changing

Ah, that is intentional: the implementation is a very cheap one which, when you right-click a highlightable subterm, selects that subterm. So if you had something else selected, it will disappear.

[Kevin Buzzard]

I have seen people moaning about this for years, so just let me comment that on ubuntu if I click in the infoview then cut and paste it has always worked absolutely fine for me.

[Patrick Massot]

Kevin, the question is how do you select what you want to copy?

[Kevin Buzzard]

click and drag?

[Kevin Buzzard]

Peek-2023-11-07-00-13.gif

What is the thing which people can't do? Is it just that I never do it, or that I have the knack and nobody else does?

[Patrick Massot]

Click and drag works, but is very painful compared to click and Ctrl-c

[Patrick Massot]

bug.gif

[Patrick Massot]

and when I wrote this has nothing to do with Widgets I mean you can also get the bug with
bug2.gif

[Patrick Massot]

Or even better:
bug3.gif

[Patrick Massot]

So it looks like any webview will trigger the bug.

[Eric Wieser]

Is this https://github.com/microsoft/vscode/issues/141080?