Code completion in vscode with mathlib4?

Stream: mathlib4

[Anand Jain]

Hello. I am trying to setup a new project that depends on mathlib.

I followed the instructions here and got the cache with lake exe cache get.

I am just wondering if code completion in the imports is supposed to work. For me it just says loading indefinitely.
Screenshot demonstrates what I mean.

Thank you. Apologies if this is the wrong channel

image.png

[Josha Dekker]

Just a quick remark about the screenshot: I think import Mathlib already imports all Mathlib. files, I’m not sure about autocompletion (as Copilot always kicks in for me).

[Julian Berman]

(Yeah, I think import Mathlib has already imported everything, but assuming your question was just in general --

I've noticed this before -- it yeah, doesn't work with Mathlib.

Something fishy is happening though, e.g. if I do import Mathlib.Data.<tab> I eventually get results (still really slowly) for that sub-package. And then once I have results, if I delete Data. and go back to import Mathlib.<tab> I also get results, again after a little while. But they look clearly incomplete.

(For Std<tab> it takes ~3 seconds on my machine, which is obviously a lot smaller than Mathlib, but still isn't instant.)