lsp and docstrings

Stream: general

[Matthew Ballard]

I haven’t used VS Code for a bit now so I don’t know if it does this. Do you see docstrings for declarations in the autocomplete pop-up menu?

[Chris Bailey]

Yeah, you have to turn toggleSuggestionDetails on first. There's a visual cue, and the shortcut is ctrl+i by default. The toggle is sticky though, so once it's on it will remain on.

[Matthew Ballard]

Next question: can you do this in emacs or vim?

[Henrik Böving]

In emacs its setting some company mode or LSP mode optioniirc

[Adam Topaz]

@Henrik Böving do you happen to know what that option is called?

[Henrik Böving]

I'm afraid not. I don't use the feature but I remember seeing it in someone's emacs in a python file with LSP

[Adam Topaz]

I would love to leave vscode behind for the correct editor (emacs), but I haven't been able to find a comfortable configuration for lean(4) just yet.

[Julian Berman]

Matthew Ballard said:

Next question: can you do this in emacs or vim?

I see:

Screen-Recording-2023-02-23-at-22.00.20.gif

Is that what you're asking for?

[Matthew Ballard]

I think that is the behavior I was asking about. My main reference point is the info from gopls the go language server where it gives, eg the signature of the function, and then the docstrings also

[Julian Berman]

When there's a signature I see it as well, e.g.:

Screenshot-2023-02-24-at-09.42.20.png

which seems to match what VSCode shows. You don't see that? It's possible I've enabled something, if you don't see it let me know and I can find what.

[Matthew Ballard]

:face_palm:

[Julian Berman]

:ambulance: