idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Wrong number of arguments to Completion at Point #550

Closed ZachFontenot closed 2 years ago

ZachFontenot commented 2 years ago
Error running timer ‘corfu--auto-complete’: (wrong-number-of-arguments (completions _partial) 0)

Hey, I'm not sure if this is how idris-mode sends completion candidates or how corfu-mode accepts completion candidates, but I'm running into this error and can't use completion at all. This wouldn't be that bad, but it seems that every time I type it tries to query for candidates and prompts this error. The open repl prints repl-completions: command not yet implemented. Hopefully soon! at every key stroke.

gallais commented 2 years ago

The open repl prints repl-completions: command not yet implemented. Hopefully soon! at every key stroke.

This suggests to me that corfu-mode hammers idris by requesting candidates for autocompletion at every keystroke.

ZachFontenot commented 2 years ago

That would seem to be the case, but I can never get completion candidates in either the repl or the idris buffer, because it always throws wrong number of arguments. When I try to press tab in the repl buffer the error throws and it eats what I've typed so far, without corfu-mode being on at all.

So I guess, should I just turn off corfu-mode when working with Idris? Does company work more fluidly? Or maybe I could try my hand at wrapping the calls and trying to pass what corfu expects for candidates.

Maybe I'm confused by how idris-mode deals with completion?

gallais commented 2 years ago

Maybe I'm confused by how idris-mode deals with completion?

As the error explains, completion is not implemented yet.

ZachFontenot commented 2 years ago

I guess I should take messages at face value. Thanks for your patience

jfdm commented 2 years ago

You can also turn of completion at point to get rid of the functionality until it is provided...

See customisation for the setting. It is called idris-completion-via-compiler