Code Completion Appears Entirely Broken

[zepalmer]

I am a new user to VSCoq. In my experience, code completion from the language server does not appear to work and generates unfilterable error notifications that interfere with my use of the tool. Code completion from the language server is off by default, so this does not affect a new user in the default configuration. I'm reporting this bug, though, in case others have a similar experience and expect the feature to work correctly.

Steps to reproduce

1. Start VSCode with a fresh configuration. I used an alternate $HOME directory as follows:
   • mkdir temp; cd temp
   • export HOME=$(pwd)
   • mkdir project; cd project
   • code .
2. Install VSCoq.
3. In VSCoq's code completion settings (press Ctrl+, and then navigate to "Extensions » VsCoq » Code Completion"), check "Enable completion suport from the VsCoq language server".
4. Create a new Coq file. (Mine was named Example.v.)
5. Type a single character into the file (e.g. "I").

Observed behavior

An error message popup appears that reads "Request textDocument/completion failed." This is VSCode's behavior whenever a code completion tool fails to produce results. The popup persists in the bottom right of the editor until the notification is cleared but will reappear when anything else is typed into the document.

Expected behavior

I expected code completion to be offered or, at the very least, no error dialog to appear.

Supplementary information

In VSCode's developer tools console, the following stack trace appears:

Can't get completions, no sentence found before the cursor: Error: Can't get completions, no sentence found before the cursor
	at /home/zpalmer/ztemp4/.vscode/extensions/maximedenes.vscoq-2.1.2/dist/extension.js:1:59738
	at ie (/home/zpalmer/ztemp4/.vscode/extensions/maximedenes.vscoq-2.1.2/dist/extension.js:1:60032)
	at /home/zpalmer/ztemp4/.vscode/extensions/maximedenes.vscoq-2.1.2/dist/extension.js:1:54816
	at Immediate.<anonymous> (/home/zpalmer/ztemp4/.vscode/extensions/maximedenes.vscoq-2.1.2/dist/extension.js:1:54836)
	at process.processImmediate (node:internal/timers:478:21)

It is worth noting, however, that writing a full sentence and then following it up with another character generates similar behavior. For instance, typing an "I" at the end of the document

Inductive foo :=
  | Foo : foo
.

produces the same error pop-up.

Environment

This example was generated using the following software:

• VSCode 1.90.1
• VSCoq 2.1.2 (and vscoq-language-server 2.1.2)
• Coq 8.18.0

[ndrewtl]

+1

[catalin-hritcu]

One of the students I teach and I can also reproduce this. My configuration is similar to the one above (VSCode 1.93.0, VsCoq v2.2.1, vscoq-language-server 2.2.1, Coq 8.18.0, on Linux), and my student's too (VsCoq 2.2.1, Coq 8.18.0, vscoq-language-server 2.2.1, on MacOS Sonoma 14.5).

[catalin-hritcu]

and I can also reproduce this with Coq 8.20.0 (and otherwise the same configuration).

[Godalin]

Same problem with Coq 8.20.0, vscoq 2.2.1, on MacOS

[gares]

Thanks for reporting.
We will look into this, but not before January

[rtetley]

Duplicate of #571
Keeping open for the conversation