Future of vscode-lean with regards to lean 4?

Stream: general

[Henning Dieterichs]

Does it make sense to contribute to the vscode-lean extension with lean 4 being on the horizon? I'm not sure I can significantly improve the infoview, but I'd love to give it a try (I dearly miss a click to insert rw ${term at cursor} feature that would allow to quickly unfold definitions). If the thing would be obsolete with lean 4, I'd wait until the release of lean 4 though.

[Mario Carneiro]

it's been on the horizon for a long time. If you have an idea, go for it

[Patrick Massot]

Yes, please. Every experimentation will be useful when Lean 4 time will come.

[Mario Carneiro]

we're not even at the point where we can assess whether things will become obsolete by lean 4

[Marc Huisinga]

it will not be obsolete. as it stands, the lean 4 lsp server has the basic architecture for making lsp work correctly, but we haven't yet invested time into the tactic side of the server. ideally, it should work so that all the neat widget stuff will still work similarly to before.

[Mario Carneiro]

right, that's a thing you would not have said had Ed thought "oh all this cool widget stuff will be obsolete in the next version, best not to try"

[Henning Dieterichs]

oh cool, then I will do some experimentations!

[Kevin Buzzard]

There was apparently a lean 4 VS Code demonstration on the Discord last Wednesday at the Cambridge lean user group meeting

[Kevin Buzzard]

I missed it :-(

[Marc Huisinga]

who demonstrated it? :o

[Kevin Buzzard]

I believe it was user Vtec234

[Marc Huisinga]

ah, wojciech :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

@Wojciech Nawrocki am I talking nonsense?

[Kevin Buzzard]

Bhavik, Shing, Ed, Eric and Fox might have been there, they were around when I arrived an hour later

[Eric Wieser]

You're not imagining it, but it was mainly a conversation about the bootstrapping of lean 4 as I remember it

[Eric Wieser]

With a quick demo to prove that trace messages from lean appear somewhere sensible

[Wojciech Nawrocki]

@Kevin Buzzard Something to keep in mind is that the state of Lean 4 editor support is rudimentary -- we are largely working out foundational/architectural details as opposed to anything user-visible. There are no features like tactic state, goto-definition, type hovers, etc. In fact, there is not even a vscode-lean4, it's just that the new server is Language Server Protocol-based so it works with any editor supporting LSP out of the box, but Lean-specific things are still a ways away.

[Edward Ayers]

Mario Carneiro said:

right, that's a thing you would not have said had Ed thought "oh all this cool widget stuff will be obsolete in the next version, best not to try"

A thought I had when deciding to do widgets was "oh lean 3 is going to be obsolete in a year anyway so I'll try it in Lean 3 and it doesn't matter if I break everything"

[Edward Ayers]

@Henning Dieterichs have you had a look at widgets? It should be possible to implement your idea entirely in Lean without any vscode extension changes. Lmk if you want any pointers

[Gabriel Ebner]

Edward Ayers said:

A thought I had when deciding to do widgets was "oh lean 3 is going to be obsolete in a year anyway so I'll try it in Lean 3 and it doesn't matter if I break everything"

It also made the decision to merge these experimental features so much easier.

[Johan Commelin]

"We're working with a sinking ship anyways. Let's blast some more holes in it."
I like this mentality, rotflol. We should apply it to proofs as well.

Me: Hey, this seems like a nice result. Let me hack a proof together.
Kernel: Ooh, don't bother. Statement looks plausible. Next!

[Henning Dieterichs]

I didn't have a look yet, but I'm definitely going to. I want to make some more progress on my lean proof first though. How would I extend the widget view from Lean? I'm quite experienced with React/TypeScript and apparently the goal view in VS Code is a react web view. Also, I have some ideas of how the abbrevation mechanism could be improved (and aligned to the emacs experience).

[Kevin Buzzard]

It's a research project, not a product. Leo always said this. I don't know if he wants lean 4 to be a product, and I've met people who won't use lean 3 because they say it's too unstable, but I am really enjoying the way people are just experimenting with the entire system at all times. We seem to be learning a lot.

[Edward Ayers]

If you are experienced with React then hopefully widgets should make a lot of sense to you.

[Henning Dieterichs]

If Lean 4 exposes a fully features syntax tree, possibly with meta information, semantic highlighting + inline type information could be implemented for VS Code easily. It would look like this: Frame-1.png

Terms of type "Prop" could be highlighted to distinguish them from non-prop-terms. Also, if only a single hypothesis or goal is changed, that goal could be rendered inline.