VSCode find symbol doesn't find many declarations

Stream: lean4

[Floris van Doorn]

I just downloaded the new Lean version 4.27.0-rc1 and updated Mathlib.
I opened a near-empty file (without imports) and I tried to find HasQuotient with ctrl+T but it could find the result.
Then I tried ctrl+T with Real or Real.add, also not finding these results
Then I opened Mathlib.Data.Real.Basic, and afterwards it can find Real in my empty file.
Similarly, if I open Mathlib.Algebra.Quotient it can find Quotient afterwards.

Other suggestions, like Real.borelSpace were available from the start.
This might have been an issue before, I just noticed it now.

**Operating system**: Linux (release: 6.1.0-0.deb11.37-amd64)
**CPU architecture**: x64
**CPU model**: 12 x AMD Ryzen 5 7600 6-Core Processor
**Available RAM**: 32.75 GB

**VS Code version**: Reasonably up-to-date (version: 1.106.3)
**Lean 4 extension version**: 0.0.221
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.1.2)
**Lean**: Reasonably up-to-date (version: 4.27.0-rc1)
**Project**: Valid Lean project (path: /local/vdoorn/projects/mathlib)
**Active Lean version**: leanprover/lean4:v4.27.0-rc1 (set by `file:///local/vdoorn/projects/mathlib/lean-toolchain`)
**Installed Lean versions**: ...

[Floris van Doorn]

cc @Marc Huisinga

[Marc Huisinga]

I can't reproduce.
Note that after starting the language server, it may take a while until all the .ileans have been loaded from disc. Until that operation is complete, you get partial results. Does the issue still occur after waiting for a while?

[Marc Huisinga]

(Also worth pointing out: after updating Mathlib, when the lean-toolchain file changed and you've got new build artifacts, the language server needs to be restarted, or otherwise it might not be able to read the .ilean files because the format changed. The VS Code extension will display a prompt to restart the server in this case and the build / fetch cache commands in the extension also always restart it.)

[Floris van Doorn]

I did restart VSCode. Is there a way to see whether the ileans-loading is complete?

I waited more than a minute (not sure exactly how long, but I believe a few minutes) on Linux.
I'll try again, and see if I can reproduce it. The behavior I saw is consistent with "it just had only partially loaded ileans", so that's probably it.

[Marc Huisinga]

It shouldn't take minutes unless there is something seriously wrong with your hardware, operating system (Windows) or anti-virus situation that significantly interferes with I/O. On my machine, the whole .ilean set of Mathlib takes a couple of seconds to load.

Could you also post one of your .ileans just to check that it has the right format, e.g. .lake/build/lib/lean/Mathlib/Init.ilean?