Julian / lean.nvim

Neovim support for the Lean theorem prover

MIT License

277 stars 26 forks source link

Replace any compe support with nvim-cmp #140

Closed Julian closed 2 years ago

Julian commented 3 years ago

nvim-compe was deprecated a bit back and replaced by nvim-cmp.

(There's also tabnine support for cmp here which may be worth trying given some success in vscode-land for Lean)

Karthik-Dulam commented 2 years ago

Currently the readme.md file conflicts on the recommended plugin to use. Under "Installation" Plug 'hrsh7th/nvim-cmp' " For LSP completion And under "Features" and in the "Recommended configuration"

Abbreviation (unicode character) insertion, can also provide a nvim-compe source.
abbreviations = {
-- Set one of the following to true to enable abbreviations
builtin = false, -- built-in expander
compe = false, -- nvim-compe source

At the moment what is the recommended plugin to use of the two?

gebner commented 2 years ago

I'd use builtin = true, I wonder if we should make that the default.

Julian commented 2 years ago

Yeah, we should. Use the builtin expander.

Julian commented 2 years ago

(I'll probably remove nvim-compe support, we can decide to add an nvim-cmp source if it turns out to be useful but I have other more important things in mind before ever thinking about it.)

Julian commented 2 years ago

263 should make this less confusing.