nvim-cmp inserting control-f character

[ram02z]

Hey, I understand that nvim-cmp is not supported as of now, but this bug is a rather peculiar one. I have just started using lean and whenever I write a begin end block, the end always gets a Control-f character appended to it. I disabled nvim-cmp entirely and I cannot reproduce this issue. I use manual completion and this occurs without having to even invoke the menu. This occurs on .lean3 files, I haven't been able to figure how to specify that .lean files are lean3 automatically.

Example file: (you could remove the end and try it yourself)

variables P Q R : Prop

example : (P → (Q → (P ∧ Q))) :=
begin
  assume p q,
  constructor,
  exact p,
  exact q,
end�

My cmp setup: https://gist.github.com/ram02z/3a5b8f26dec39d46345b22c7445cd386

My lean.nvim setup:

require("lean").setup{
  lsp3 = { on_attach = on_attach },
  lsp = { enable = false },
  mappings = true,
}

Neovim version:
NVIM v0.6.0-dev-gb3e0d6708

[Julian]

It's not "supported" only in the sense that no direct integration exists, but definitely it's supported in that if you're using it we shouldn't break things :P

I'm not sure what's happening here, I haven't myself managed to switch to cmp yet, so we'll have to investigate.

Of course if you figure out what's happening please feel free to let us know (or of course send a PR :)

Just to be sure, you don't happen to have both compe an cmp installed perchance right?

[ram02z]

Just to be sure, you don't happen to have both compe an cmp installed perchance right?

Nope, I uninstalled compe when I switched. I honestly dont even know how it is cmp because I don't invoke completion at all and it still persists, but when I did uninstall it, it did fix my issue.

[Julian]

OK now that I've switched to cmp (which was pretty painless) I can certainly confirm this issue at least, even if I haven't figured out what causes it yet. I suspect something in cmp is interacting badly with us, maybe having to do with some code in it that's trying to detect endwise-like things, but yeah shouldn't be too hard to find with a bit of digging I suspect.

[Julian]

This is an upstream bug AFAICT -- filed it on nvim-cmp (it's easily reproducible without lean.nvim). It should be easy to fix but I couldn't see precisely how to do so yet without staring at what that code is trying to do a bit more.

[Julian]

Ok and it's been fixed already :)

[ram02z]

Ok and it's been fixed already :)

Hmm, I can still reproduce the issue.

[Julian]

Sorry, I didn't try it out before making assumptions but looks like indeed you're right, that didn't do it. Will reopen upstream (it's still the same issue it appears with indentkeys + nvim-cmp).

[Julian]

OK, the second fix seems to work here -- does it for you as well?

[ram02z]

OK, the second fix seems to work here -- does it for you as well?

Yeah the fix works now, thanks!

[ram02z]

After hrsh7th/nvim-cmp#443, the same issue is back.

Why do we append indentkeys instead explicitly setting it? (I am asking because I don't understand the default indentkeys values)

https://github.com/Julian/lean.nvim/blob/main/indent/lean3.vim#L6

[Julian]

Some of what's there is still applicable (like inserting a {) though yeah we could just set the whole thing, it doesn't matter too much, really we need better indentation in general, what's there was a quick hack for the most common case (which is #38).

But really again this is a nvim-cmp issue unrelated to us (which has to do with various possible values for indentkeys) so we should take the issue upstream.