Zulip Chat Archive

Stream: general

Topic: namespaces in VSCode


Eric Rodriguez (May 18 2021 at 18:18):

is there some way to see what namespace a function is in in VSCode easily? it would be nice to not have to ctrl+f around a file to figure out what it's in

Kevin Buzzard (May 18 2021 at 18:21):

If it's not being defined, then hovering over it might well work. If it is being defined, I usually write #where just above the definition (which is imported for the kinds of mathlib files I usually am dealing with)

Eric Rodriguez (May 18 2021 at 18:24):

ooh, #where is exactly what I was looking for - thanks!

Eric Wieser (May 18 2021 at 18:58):

How hard would it be to build lean server support for this? The only approach I've come up with so far is temporarily adding #where to the source and then removing it again; but that feels like a nasty hack

Alex J. Best (May 18 2021 at 21:13):

Don't the lean4 breadcrumbs for vscode lean4 plugin, do exactly this? So it definitely seems possible, maybe backportable?

Adam Topaz (May 18 2021 at 21:14):

That's an LSP thing

Adam Topaz (May 18 2021 at 21:14):

(I think)

Kevin Buzzard (May 18 2021 at 21:18):

In VS Code I can't seem to tell the difference between a section and a namespace -- they both show up the same in breadcrumbs? (if I've understood correctly what a breadcrumb is). I have recently started the habit of calling my sections with "descriptive" names like comm_ring_lemmas as opposed to comm_ring, so I can see that they're not namespaces when I see stuff like end comm_ring_lemmas.

Sebastian Ullrich (May 18 2021 at 21:22):

Yeah, we should probably use different icons for namespaces and sections in the breadcrumb bar

Eric Wieser (May 18 2021 at 22:08):

The L in LSP is "Lean", as opposed to the Microsoft "Language Server Protocol", right?

Adam Topaz (May 18 2021 at 22:10):

Eric Wieser said:

The L in LSP is "Lean", as opposed to the Microsoft "Language Server Protocol", right?

Is it? I was referring to the generic language server protocol

Eric Wieser (May 18 2021 at 22:13):

This is why I'm confused!

Eric Wieser (May 18 2021 at 22:21):

But yes, I understand how to tell vscode where the sections are; what I can't work out is how to get the server in leanprover-community/lean to translate a cursor position into a namespace name

Eric Wieser (May 18 2021 at 22:23):

#where has access to the parser state by virtue of having been parsed

Eric Wieser (Jun 09 2022 at 12:23):

I PR'd this for lean 3 as https://github.com/leanprover/vscode-lean/pull/305

Eric Wieser (Jun 09 2022 at 12:24):

image.png

Alex J. Best (Jun 09 2022 at 12:35):

How does it work?!

Eric Wieser (Jun 09 2022 at 12:55):

It only knows how to tell you the name of the current lemma, and deduces the namespace from that

Notification Bot (Jun 28 2022 at 11:11):

38 messages were moved here from #rss > Recent Commits to mathlib:master by Eric Wieser.


Last updated: Dec 20 2023 at 11:08 UTC