No autocompletion when typing even number of characters in VSCode

[tydeu]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

With VSCode, typing an even number of characters does not trigger autocompletion (the Lean 4 server produces no results). If the user has "Word Based Suggestions" in VSCode enabled, the editor will fall back to such suggestions, preventing any further attempts at intelligent autocompletion from the Lean 4 server.

Steps to Reproduce

#check B -- completion results on typing 'B'
#check Ba -- if typed together, no results; if typed as 'B' then after results, 'a', then results
#check Bas --  if typed together, results; if typed as 'B' then 'as', no results
#check Base -- if typed together or as 'Ba' then 'se', no results; if typed as 'B' then 'ase' or  'Bas' then 'e', results

Expected behavior:

Autocompletion regardless of the number of characters typed.

Actual behavior:

No autocompletion when typing an even number of characters.

Reproduces how often:

Always.

Versions

VSCode 1.73.1
Windows 10 20H2
Lean (version 4.0.0-nightly-2022-11-10, commit 2386c401d231, Release)

Additional Information

Bug first reported on Zulip and confirmed by @Kha and Kevin Buzzard.

[Kha]

Relevant docstring from rust-analyzer: https://github.com/rust-lang/rust-analyzer/blob/9ba55bad4f37edb58379ca72f4bcd6684c36e9e1/lib/lsp-server/src/msg.rs#L122-L126