Extremely slow when importing Mathlib

Stream: new members

[Luiz Kazuo Takei]

I've been playing with the different parts of Mathlib but one issue has been slowing down my learning considerably.

Sometimes I think I need to import a certain part of Mathlib and when I try to do that, it takes a veeeeery long time. The thing is I am not even sure I need this part of the library, I am just testing.

For instance, now I am trying to use the notation ∑ and I am not sure which part of Mathlib I need. I saw a file in Mathematics in Lean that uses ∑ and they do a import Mathlib.Tactic. So I tried to do that. I've been waiting for more than 1 hour now for VSCode to finish importing that...

1. Is this normal?
2. Any tips on how to speed up the learning process?

[Kenny Lau]

have you run lake exe cache get to get the precompiled files of mathlib?

[Ruben Van de Velde]

That's not normal, unless you're on a very low-powered computer

[Mohamed Talaat Harb]

so, I actually had similar experience when I used the latest version of mathlib4 in my configuration for the project . I think the reason is that the pre-compiled 'cache' will definitely end up outdated so it will either slow down to download new ones or to use the code and compile it on the fly which is also slow.

but when I switched my project configuration to a concrete version of mathlib4 (in that case it was "v4.15.0") I ended up with very fast imports, server restarts, compiles.

[Kevin Buzzard]

Are you not downloading mathlib cache with lake exe cache get? You shouldn't be compiling mathlib yourself, that takes an hour. We already compiled it for you.

[Luiz Kazuo Takei]

Thank you @Kenny Lau and @Kevin Buzzard.

How often should I run exe cache get? For instance, if I change the imports of a file, do I need to run that again?

[Kenny Lau]

are you editing mathlib?

[Kenny Lau]

if you're editing mathlib for a PR, then every time you publish the edit, github will automatically make a compiled version after half an hour, and then you can run lake exe cache get to get the updated compiled version;

otherwise, you shouldn't be editing mathlib at all

[Luiz Kazuo Takei]

Thanks for the tip @Mohamed Talaat Harb!

From what I saw, this can be done in lean-toolchain. Is that correct?

In my case, it has this: leanprover/lean4:v4.25.0-rc2.

[Kenny Lau]

if this is an external project depending on mathlib then you only need to run lake exe cache get once (or every time you update the mathlib version)

[Ruben Van de Velde]

No, you don't want to touch lean-toolchain on your own

[Ruben Van de Velde]

Again, it depends on whether you're making changes inside mathlib or in a project that depends on mathlib

[Luiz Kazuo Takei]

I am not touching Mathlib. I am just importing it.

[Kevin Buzzard]

Then you only run lake exe cache get once.

[Ruben Van de Velde]

(Unless you've run lake update, but don't do that before you know what it does :))