Zulip Chat Archive

Stream: lean4

Topic: state of the vscode extension


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Mar 21 2021 at 13:24):

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

view this post on Zulip 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.

view this post on Zulip 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: May 18 2021 at 23:14 UTC