Slow autocomplete after an import

Stream: general

[gldanoob]

If I import files from Mathlib and start using autocomplete, the results often take seconds to load, which is much slower compared to Lean 3. For example, if I type

import Mathlib.CategoryTheory.Category.Basic
open CategoryTheory

variable {C : Type} [Cat

I will have to wait for seconds before Category shows up in the popup. In contrast, the suggestions show up instantly without any imports. I made sure I ran lake exe cache get, and the imports are resolved without delay but not the LSP suggestions. Is this behavior normal?

[Yongyi Chen]

This happens to me too. I'm not an expert but I know other programming languages don't suffer from this problem, e.g. clangd for C++ even when importing the entire standard library (which is huge) is pretty instant. I suspect instances are the reason this can't be super-fast?

[Mario Carneiro]

No, I don't think there is any irreducible reason for this not to be fast

[Yongyi Chen]

Oh, is this being worked on then? A fast autocomplete would be a very large QOL.

[Mario Carneiro]

I don't know, it depends on a diagnosis of exactly what the time is being spent on. Maybe @Marc Huisinga might be interested to look into this?

[Mario Carneiro]

@Sebastian Ullrich do you know how best to benchmark or profile something like this?

[Sebastian Ullrich]

Just running perf top in the background is great for a first impression. But it's most likely the fuzzy matching code.

[Sebastian Ullrich]

I think this is the first user complaint I have seen since it was introduced

[David Loeffler]

Sebastian Ullrich said:

I think this is the first user complaint I have seen since it was introduced

Well, here's a second one – I also find that the auto-complete in lean4 is much, much slower than it was in lean3, to the point of being almost unusable.

[Yongyi Chen]

Yeah, I think the lack of complaints was due to everyone understanding that this (in particular, the vscode extension) is still preliminary work in progress.

[Sebastian Ullrich]

Unfortunately that assumption is dead-wrong in this case so it's better to complain (or even better, open an issue) than to assume