LSP autocomplete quirks

Stream: new members

[Graham Leach-Krouse]

I'm trying to understand some quirks in where LSP autocomplete seems to be available. Some of these may be artifacts of my particular setup (lean.nvim, nvim-cmp,lean4:nightly-2023-06-20), but I'm not sure. Here's a fairly simple piece of weird behavior that seems to be reproducible. If I trigger autocomplete at the end of this snippet:

theorem succPlus : ∀n m : Nat, n + Nat.succ m = Nat.succ (n + m) := by
  apply Nat.

then I don't get any lsp autocomplete suggestions. But if I trigger it at the end of this snippet:

theorem succPlus : ∀n m : Nat, n + Nat.succ m = Nat.succ (n + m) := by
  exact Nat.

I get autocomplete suggestions from the Nat namespace (this seems like desirable behavior from my PoV). If I add a single character after the end of the first snippet above, (so that it ends Nat.a, for example), then I get LSP suggestions on autocomplete again.

Is this just somehow some misconfiguration on my end? A quirk of neovim toolchain I'm using? Or is there some reason for the difference?

[Bulhwi Cha]

@Graham Leach-Krouse I also get this behavior on my Doom Emacs.

Screenshot_20230701_234647.png
Screenshot_20230701_234804.png

[Graham Leach-Krouse]

Thanks. That suggests that it's something (intended or unintended) with the language server, rather than the editor toolchain.