Unable to use autocompletion.

[120ace]

I cannot seem to get autocompletion to work at all. Any help would be appreciated.

[mattpolzin]

Since auto-completion will work the same way as it does for other LSP-based integrations, do you have auto-completion working for any other languages that use LSP? There are at least a few ways to set auto completion up in Neovim so it would be best to know it is working in the general case before troubleshooting Idris2 in particular.

As far as Idris2 in particular goes, there is one pretty big gotcha — the LSP server only works if you’ve got an ipkg file for the project you are editing. If you don’t, then auto-completion (along with all the other LSP functionality) does not work.

[120ace]

Sorry for the late reply.

As I was typing out this reply, I decided to reread the help file for your plugin. In doing so I realized I had missed the section that stated how to pass my setup directly to the lsp using the server function. I corrected that issue and now do have some autocompletion. However, I am not sure if I am getting the correct results back.

This is what it currently looks like: https://asciinema.org/a/HWNDc0TSuwFpf0G7KePmc4mUR
I have no prior experience with this, and I am just now trying to learn idris2.

Thanks for the help.

[120ace]

I forgot to add, I am manually triggering the shortcut to check for completion options, it is not automatically suggesting them as I type. IDK if that helps.

[mattpolzin]

Your results look good to me at a glance; what about them is fishy to you? If it’s the way that autocompletion puts the function call in parents and adds holes for you, that is the way it is supposed to work. It’s been a feature request for the Idris2 LSP to support the more normal autocompletion where you just get the name of what you are typing without assuming you are invoking the function with all its arguments.

[120ace]

Just a preface, I am pretty new to all of this, the depth of my experience with idris2 is (currently) just going past the hello world part of (https://github.com/stefan-hoeck/idris2-tutorial). Really, the only language/lsp I am thoroughly familiar with is lua/lua_ls.

• I am confused about how the lsp is inserting the function. For example, when I was trying to insert putStrLn, what it gave me was (putStrLn ?putStrLn_arg_0). What I am used to, I.E. using lua_ls, is that when inserting a function It just inserts the function's name, and if there is a snippet for it, inserting the snippet and allowing me to jump through it while typing.
  I was wondering if the ?putStrLn_arg_0 was supposed to be placeholder text for a snippet; however, I cannot seem to jump through it as though it was one. Is this just a problem with my setup, how the lsp works by default, or something that nvim cannot make use of?

• when typing, the autocompletion was not coming in automatically while just typing, I was having to manually trigger nvim-cmp to check for autocompletion of the word I was on; it would then stay on as I continued typing the word.

• the suggestions for the autocomplete menu seem to be case-sensitive. For example: typing putstr, and manually triggering cmp for completion, doesn't give any autocompletion items, while typing putStr will.

• when I was trying the autocompletion for types, I couldn't find results for the type of Integer.

[mattpolzin]

?putStrLn_arg_0 is called a hole. It’s a language feature in Idris and it’s like a template argument except the hole is a valid part of a program; the compiler can tell you its type and help you “fill” the hole whenever you want to at some point in the future. It would be nice if this also was the type of template thing the editor jumped through but I am not familiar enough with LSP to say if we can have it both ways. The idea to have it just auto-complete the function name is the thing I was mentioning is an existing feature request for the LSP but not currently implemented.

[mattpolzin]

Your last two bullets would probably be good feature requests for the idris LSP if they aren’t already tracked over there. I’m not totally sure if case insensitivity is desirable to everyone but if so it would be a matter of code changes to the server.

[mattpolzin]

I’m not sure what the Lua LSP could be doing differently than the Idris one (or the nvim plugin, more likely) to cause auto-completion to show up while typing rather than on demand. I’ve got my Idris auto-completions showing up as I type but as I recall that was something I got automatically when I set cmp up to have an nvim_lsp source.