Zulip Chat Archive

Stream: lean4

Topic: state of the vscode extension


Daniel Fabian (Mar 19 2021 at 13:58):

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 (Mar 19 2021 at 14:36):

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 (Mar 19 2021 at 14:38):

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 (Mar 19 2021 at 15:03):

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

Daniel Fabian (Mar 21 2021 at 13:22):

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 (Mar 21 2021 at 13:24):

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

Sebastian Ullrich (Mar 21 2021 at 13:31):

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 (Mar 21 2021 at 13:37):

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.


Last updated: Dec 20 2023 at 11:08 UTC