The copy buttons in VScode InfoView have disappeared

Stream: new members

[Ching-Tsun Chou]

There used to be copy buttons shaped like the double-quote sign in VScode's Lean InfoView that, when clicked, copy the corresponding message (such as the tactic state) into the Lean file as a comment. But today I can't find them anymore. What happened? Did something in Lean or VScode change?

I use that feature very often to scrutinize the tactic state and to set up have tactic goals.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

They have been deleted in vscode-lean4#606 in order to clean up the UI; you can still use the default copy functionality present in the webview, though (ctrl-c or cmd-c or right click+copy).

[Ching-Tsun Chou]

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 What is the webview you are referring to? How do I invoke and use it?

More generally, why are such useful features removed without notice? Such major changes should have been discussd in the Zulip first. There are users depending on them.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Ching-Tsun Chou I just mean that in the infoview, you can select a piece of text just like in the browser, and right-click -> copy (or use a keyboard shortcut). (I agree with you that inserting it as a comment is less ergonomic now because it requires more clicks/actions.)

[Ching-Tsun Chou]

Having to select and copy text is not only very annoying, but the old feature also puts the copied text conveniently in a comment. Now I have to manually fall back to an earlier version of the extension.

How can this kind of significant changes be made without discussion or even an advanced notice? Who is responsible for VScode's Lean4 extension?

[Ching-Tsun Chou]

I filed an issue: https://github.com/leanprover/vscode-lean4/issues/614

[Ching-Tsun Chou]

To all: If you agree with me that those buttons should be restored, please comment here and/or in the vscode-lean4 issue I opened (see above). Thanks in advance!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

On the contrary, please do not comment on the GitHub issue just to agree with the request; please use the upvote (:+1:) reaction instead.

[Yaël Dillies]

@Ching-Tsun Chou, do you already use the Error Lens vscode extension? If not, I would suggest trying it out to see whether that covers your use case of the former copy buttons

[Ching-Tsun Chou]

@Yaël Dillies Are you referring to the following extension?
https://marketplace.visualstudio.com/items/?itemName=usernamehw.errorlens
I installed it and nothing seems to happen. How do I, for example, copy the current tactic state when my cursor is in the middle of a tactic proof?

[Kevin Buzzard]

I think Yael is just saying "now if you don't end your proof with sorry you'll get an error telling you the tactic state in the pane containing the Lean file, will this do?"

[Yaël Dillies]

And yes that's the correct extension

[Ching-Tsun Chou]

I see what you mean. It doesn't really help. First, I need to invoke a particular VScode command to copy it, which makes it no easier than manual select-and-copy-paste. Second, I have more use cases than just getting a copy of the last proof state; see:
https://github.com/leanprover/vscode-lean4/issues/614#issuecomment-2838002685