Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Help for a newbie #320

Closed ykonstant1 closed 9 months ago

ykonstant1 commented 9 months ago

Hello; I am trying to move to Neovim in order to use your plugin for Lean 4. However, I seem to be unable to reproduce the features you demonstrate in your video.

My neovim version is : NVIM v0.9.4 Build type: Release LuaJIT 2.1.1699392533

I am using init.vim which I copied almost verbatim from my vim file, so I am not using (or know how to use) lua code.

I added all the required and recommended plugins via vundle. Then I copied the recommended configuration from your "full configuration" section as follows:

 lua <<LUA
    #code follows 
LUA

at the end of my init.vim

I got the infoview working correctly, some error indications working, but there are no hovering messages or menus and no suggested autocompletions, for instance Array. dropping a list of array actions. The last one in particular is crucial for my Lean programming.

Can you help with this? I must be doing something completely wrong, but I have no idea what.

Julian commented 9 months ago

Hi! Happy to help. Might be easier to do it interactively via Zulip, but either works --

Broadly I'd suggest maybe looking at this page in the wiki which might be a bit friendlier to start -- and complain if something still isn't clear enough!

But separately/specifically, here's perhaps some initial help:

I got the infoview working correctly, some error indications working

Cool, this likely means the plugin is working at least.

For the rest of the below you may find my LSP dotfiles file relevant as it contains most of what I'll share for the rest. Specifically a few will go in the on_attach handler you passed in to lean.nvim -- which if you didn't pass one in yet may explain some issues. Mine you can see at that link.

there are no hovering messages or menus

This is done via vim.lsp.buf.hover (try running :h vim.lsp.buf.hover just to see the LSP docs if you haven't ever looked at those, they're pretty decent). I have that Lua function bound to K, which matches the "vanilla" vim behavior of showing documentation with K. If you like that, you can use:

vim.keymap.set('n', 'K', vim.lsp.buf.hover, { noremap = true, buffer = true })

at which point if you hit K in normal mode you should see a popup. Make sure the above is inside your lua << block if not in a lua file -- and really as I say you should have it inside the function you pass to on_attach as I did (and as the wiki page hopefully shows).

and no suggested autocompletions, for instance Array. dropping a list of array actions

Have you installed nvim-cmp? It's not strictly speaking a dependency of this plugin, you can use any completion plugin you'd like, albeit I assume no one uses anything but that one as it's the most popular neovim one by a decent margin. So make sure you have that installed and set up (you'll have to follow its instructions there). Or the wiki page has a sample setup for it which should work.

After that I think you should at least have these things working.

ykonstant1 commented 9 months ago

Thank you so much for the detailed help; I will go through it slowly, in order to avoid further mistakes on my part, and report back!

Julian commented 9 months ago

(Going to close this assuming you hopefully are up and running but speak up here or there if you still need help! Happy Leaning!)