Zulip Chat Archive

Stream: new members

Topic: The copy buttons in VScode InfoView have disappeared


Ching-Tsun Chou (Apr 28 2025 at 23:01):

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.

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Apr 29 2025 at 02:47):

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 (Apr 29 2025 at 03:20):

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 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.

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Apr 29 2025 at 03:30):

@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 (Apr 29 2025 at 03:43):

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 (Apr 29 2025 at 04:46):

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

Ching-Tsun Chou (Apr 29 2025 at 05:09):

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!

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Apr 29 2025 at 05:28):

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 (Apr 29 2025 at 06:15):

@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 (Apr 29 2025 at 08:26):

@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 (Apr 29 2025 at 08:48):

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 (Apr 29 2025 at 09:01):

And yes that's the correct extension

Ching-Tsun Chou (Apr 29 2025 at 09:07):

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


Last updated: May 02 2025 at 03:31 UTC