search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
276 stars 26 forks source link

Error while calling lua chunk: ~/.config/nvim/plugin/lean.lua:10: module 'cmp' not found #285

Closed mdgeorge4153 closed 1 year ago

mdgeorge4153 commented 1 year ago

I attempted to workaround #284 by commenting out the "optional dependencies" listed in https://github.com/Julian/lean.nvim/wiki/Getting-Started#install-leannvim-and-its-dependencies. I now get a different error when starting nvim:

Error detected while processing ~/.config/nvim/plugin/lean.lua:
E5113: Error while calling lua chunk: ~/.config/nvim/plugin/lean.lua:10: module 'cmp' not found:
        no field package.preload['cmp']
        no file './cmp.lua'
        no file '/usr/share/luajit-2.1.0-beta3/cmp.lua'
        no file '/usr/local/share/lua/5.1/cmp.lua'
        no file '/usr/local/share/lua/5.1/cmp/init.lua'
        no file '/usr/share/lua/5.1/cmp.lua'
        no file '/usr/share/lua/5.1/cmp/init.lua'
        no file './cmp.so'
        no file '/usr/local/lib/lua/5.1/cmp.so'
        no file '/usr/lib/x86_64-linux-gnu/lua/5.1/cmp.so'
        no file '/usr/local/lib/lua/5.1/loadall.so'
stack traceback:
        [C]: in function 'require'
        ~/.config/nvim/plugin/lean.lua:10: in main chunk
"fin.lean" 36L, 1228B

I imagine one of those dependencies is loading something that lean.vim needs but isn't marked as a dependency of lean.vim.

Julian commented 1 year ago

This sounds like you removed the lines to install cmp but you're still trying to require it in your own lean.lua file. Delete those lines too if you're not intending to use cmp.

Julian commented 1 year ago

Let me know if that doesn't help.