Jump to definition in Vim

Stream: new members

[Simon Jacobsson]

Hello,
I would like to be able to, in vim/neovim, jump to the definitions of the functions I use. Lean is not supported by ctags, so I can't use it to generate tags. Is there some other way to generate tags for Lean or to get the "jump to definition"-functionality?
I know Julian has this functionality in lean.nvim, but I don't want all of the other stuff his plugin has.

Best,
Simon

[Patrick Massot]

I think that "not wanting all the other stuff this plugin has" isn't a wise move. And I'm sure you can opt out of certain things if it does a bit too much.

[Simon Jacobsson]

Okay, so you are not aware of any other way of doing it, @Patrick Massot ?

[Patrick Massot]

No.

[Simon Jacobsson]

Okay, thanks for the input

[Mauricio Collares]

Did you stumble upon https://github.com/rish987/lean_ctags?

[Simon Jacobsson]

This looks like it could be useful, will take a look!

[Julian Berman]

I agree with Patrick, even grudgingly :), since before I wrote the plugin I thought I was ok with very minimal things -- but even if you want to go your own way, I think you'll be happier with LSP support rather than just ctags, since it will give you more accurate jump to definition, even if you choose to do nothing else. You can do this "directly" with nvim-lspconfig, since we were sure when writing lean.nvim to contribute that upstream. Of course on the other hand if you do choose to still use lean.nvim, as Patrick says, if you want to turn everything off (the infoview, say), it's perfectly well supported and essentially leaves you in the same state but with the ability to add in other functionality later. E.g. using Lean without abbreviations support is not much fun. But do what makes you happy :)

[Simon Jacobsson]

Maybe you guys are right.
I have also tried setting up lean.nvim but could not get the LSP to connect. That is likely a problem on my part though. I may try again this weekend.

[Julian Berman]

If you have setup issues please share/complain about them -- I think the install instructions are clear but if they aren't I very much want them to be. The most likely reason for the LSP not connecting is not installing lean-language-server. But yeah let me know.

[Simon Jacobsson]

I knew I had lean-language-server installed. But will try again and open a new topic if I get the same problem!

[Pedro Minicz]

There is a VSCode extension called VSCode Neovim (https://github.com/vscode-neovim/vscode-neovim/) which I'd highly recommend for Vim/Neovim users. It embeds Neovim inside VSCode (unlike VSCode Vim which only emulates Vim behavior inside VSCode) and it works perfectly with the Lean extension.

With the extension, if you press K in normal mode, a small window with type information and some documentation about the term under the cursor will appear. If your cursor is over a tactic, a small window with documentation about the tactic will appear instead. This shortcut has exactly the same effect as hovering the mouse over the term/tactic (with the added bonus of not having to take your hands away from the keyboard). This is example of the Neovim extension working perfectly with the Lean extension, because K is a Vim/Neovim normal mode shortcut that opens the manual page for the word under the cursor.

Also like in Vim/Neovim (particularly, like in the help files), you can press <c-]> (ctrl+]) to jump to the definition of the term/tactic under the cursor in normal mode. Again like in Vim/Neovim, you can then press <c-o> and <c-i> to jump forwards and backwards in the cursor position history, even between multiple files, making it extremely easy to jump to a definition, then another, then another, then back to your own code. Another example of the Neovim extension working perfectly with the Lean extension (and more convenient than pressing <f12>)!

I've used this extension ever since I started using Lean. As far as I can tell it behaves perfectly well together with the Lean extension and it makes using VSCode almost exactly like using Vim/Neovim (almost, see https://github.com/vscode-neovim/vscode-neovim/issues/936 for one of the rare examples where it doesn't act exact like Vim/Neovim).

I think this extension (or maybe even the more popular Vim emulation extension VSCode Vim) should be mentioned in https://leanprover-community.github.io/get_started.html or another page that a beginner is likely to read when getting started with Lean. Since Lean doesn't have an official Vim/Neovim extension, it would be nice to inform people that they can get the best of both words with this VSCode extension. People who use Emacs or Vim/Neovim get so much convenience out of their editor that I perfectly understand why some may rather sacrifice the convenience of a proof assistant extension instead of sacrificing the convenience of their (amazing, objectively superior) text editor.

[Julian Berman]

You're probably right to point it out as a good option. For what it's worth, all the things you mention work with lean.nvim too :P, so I'd like to think at this point it's a good option too. But I also think as Lean is growing we'll grow more and more good options, competition (and choice, and symbiosis) is very very good.

[Julian Berman]

Idly by the way, on your vscode-neovim ticket --

ctrl+m in any mode behaves exactly the same way as enter.

This isn't 100% true anymore, or at least it optionally isn't true. neovim now supports CSI, and if your terminal supports it, as e.g. Kitty does, the keys are separate -- I have no idea what kind of terminal emulation support vscode is going with, but it should likely at least consider doing something like that as well.

[Pedro Minicz]

@Julian Berman very interesting, I was unaware of that. I guess my claim about ctrl+m only applies to more traditional terminal emulators then.

I'll definitely check lean.nvim out too. Although VSCode Neovim is pretty good, I honestly rather just one Neovim. :grinning_face_with_smiling_eyes: