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):
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