state of the vscode extension

Stream: lean4

[Daniel Fabian]

I was wondering if there's a backlog or some requests for features for the lean4 extension. One thing I noticed, playing around with lean 4 is that the extension is really not on the same level as the lean 3 one (unsurprisingly). And it is something that, I think, creates unnecessary barriers for trying out lean 4.

E.g. the proof state could be visible more broadly, doc comments on hover, possibly a more powerful go to definition (at an import), stuff like that.

[Sebastian Ullrich]

Doc comments on hover should already work. Better go to definition is on the Lean side, https://github.com/leanprover/lean4/issues/287

[Sebastian Ullrich]

What do you mean by "visible more broadly"? If you have simple suggestions to enhance the UI or UX, I think we're all ears. Otherwise "do at least as well as Lean 3" is of course already a goal.

[Daniel Fabian]

well a obvious one would be to show the proof state not only in tactic mode but also in term mode.

[Daniel Fabian]

One thing I'd like to be able to do and I don't currently have a good way with lean 4, I think is this.

How do I know what the proof state is after a tactic ran? In lean 3, I'd do a hack like this: { split, left, right, simp, tautology, } notice the trailing ,. It allows me to see the state after a tactic has finished.

To be honest, I didn't like it in lean 3 either, but at least I could tell what the tactic did.

Do you think we could build something that makes it easy to know what the state after the tactic is?

[Sebastian Ullrich]

The state shown in the info view is the one after running the tactic

[Sebastian Ullrich]

Conversely, it is not possible to view the initial state of a tactic proof branch (with at least one succeeding tactic) without editing the file, though we can fix that by showing it on by, =>, etc.

[Daniel Fabian]

ok, right. I think my terrible hack so far was by {} and then I'd see the result on the closing brace or something. Either way, seeing both would be really nice.