Autocomplete not working, vscode falls back to the default.

[kspalaiologos]

Description

I would have expected lean4 vscode extension to let me autocomplete existing theorem names and imports, but this is not the case - vscode falls back to its default word-level autocomplete. See e.g.:

Other parts of the extension work, like the error squiggles, syntax highlighting and the right pane.

Versions

vscode-lean: v0.0.118.

 % lean --version
Lean (version 4.2.0-rc4, commit 819b5eaceaa4, Release)
 % uname -a
Linux laplace 6.5.0-4-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.5.10-1 (2023-11-03) x86_64 GNU/Linux

[mhuisi]

Import auto-completion is leanprover/lean4#2655 and will likely be merged soon. For the other limitation, you may want to create a separate issue in the lean4 repo.

[mhuisi]

The former part of this is done now and will be in the next release.