Widgets in vscode

Stream: lean4

[Gabriel Ebner]

I have just merged @Wojciech Nawrocki's PR that enables widget support in the vscode extension. This will most likely break something, so please keep an eye out for new bugs and complain here or on the bugtracker if you find one!

[Gabriel Ebner]

Now we just need an elisp guru for the last remaining editor...

[Sebastian Reichelt]

Not sure if it's related, but the timing matches quite well. On my machine (VSCode on Linux), the infoview now stops updating after a while. The "Problems" tab still updates properly, but the infoview is stuck in some state, usually empty. Here's a screenshot: https://imgur.com/RrHLi7w.png

[Gabriel Ebner]

This might be the same issue as https://github.com/Julian/lean.nvim/issues/176
Do you remember how you got into the stuck state? It would be awesome for debugging if we could reliably reproduce this.

[Sebastian Reichelt]

Unfortunately not, except that I can reliably reproduce it by working for 5-15 minutes. ;)

[Julian Berman]

If you can indeed manage to get it into the stuck state and can come back and interactively debug while you're in the stuck state that may also help all of us figure it out -- e.g. by enabling logging and seeing what chatter is going from VSCode -> lean, or stracing the language server process and seeing what it's doing, or something.

[Sebastian Reichelt]

I've just noticed that in one of my files, it reliably happens almost immediately after opening. More specifically, only the first click works, then it gets stuck. It's a particularly heavy file; that might be part of the reason. If someone else wants to try it with the same file, the project is at https://github.com/SReichelt/universe-abstractions, and the particular file is FunctorUniverse.lean.

[Heather Macbeth]

Is there any plan to bring the Lean 3 infoview widgets to Lean 4? I particularly miss the buttons which displayed on the pop-up from clicking a subterm in the infoview: (1) jump to the definition of the leading function application, (2) copy the whole subterm, (3) close the pop-up.

[Mario Carneiro]

jump to definition is already there, close the popup should hopefully be a lot more automatic than it used to be

[Mario Carneiro]

For "copy the subterm", one relatively unimposing way to do it would be to have clicking on a hoverable term (such that the term has a highlight and the hover itself may or may not be shown) select the text, and then you can just ctrl-C copy it

[Patrick Massot]

Heather, jump to definition is there as an Easter egg, you need to know the secret code which is Ctrl-click.

[Patrick Massot]

I agree that the copy-paste button is needed. And it would be good to have a smart one (providing something that is more likely to elaborate than what is displayed).

[Heather Macbeth]

Thanks Patrick. Indeed I didn't know about the Ctrl-click.

[Patrick Massot]

It also took me forever. I think I had to ask Ed and he revealed this secret to me. It has been here for ever, hiding in plain sight.

[Heather Macbeth]

Less important, but I also think the display in Lean 3 is visually clearer. It gives more prominence to the type of the term (which is often what I want to know): it displays as say

ℝ
3 * a + b ^ 1.5

rather than

3 * a + b ^ 1.5 : ℝ

Does anyone else share my appetite for requesting a change on that?

[Wojciech Nawrocki]

Patrick Massot said:

It also took me forever. I think I had to ask Ed and he revealed this secret to me. It has been here for ever, hiding in plain sight.

Yeah.. the hope was that for people who already use VScode where ctrl-click is the default way of jumping to a definition via mouse, this would be "obvious" so they wouldn't even have to think about it. Clearly that's not the case though, especially for people who use the keyboard or the right-click menu. I do think the new UX is better because you can jump to the leading function without even opening a popup, but it needs to be more discoverable. Maybe we need a (?) button that shows a small tutorial.

[Kevin Buzzard]

Patrick Massot said:

It also took me forever. I think I had to ask Ed and he revealed this secret to me. It has been here for ever, hiding in plain sight.

I also discovered this easter egg from Ed -- I bumped into him in person a couple of months ago and moaned about its absence and he told me the secret :-)

[Wojciech Nawrocki]

For "copy the subterm", one relatively unimposing way to do it would be to have clicking on a hoverable term (such that the term has a highlight and the hover itself may or may not be shown) select the text, and then you can just ctrl-C copy it

This is a good idea, except that currently clicking on a subterm also opens a popup. Not sure that clicking should do two things at once since you may not always want to both select something for copying and open the popup

[Wojciech Nawrocki]

Does anyone else share my appetite for requesting a change on that?

Implementation-wise this would be a trivial change; it's just a matter of what the community prefers

[Kevin Buzzard]

In Lean 3 cut-and-paste from the infoview was hit-and-miss (and apparently even more hit and miss on Windows), but in Lean 4 I've had no problems. Like Heather I today wanted to see the type of a (large) expression (I wasn't sure if it was Prop or Type) and it was a little annoying than clicking on it in the infoview didn't immediately just tell me the answer, so I had to use my brain.