Slow import

Stream: mathlib4

[tau]

import Mathlib takes several minutes on my machine (MBP 2020 with M1). I found #24020 from which I concluded that cached builds are not optimized for my machine and decided to rebuild mathlib manually (which took almost 8 hours), but that didn't help. Is there anything I can do to speed up mathlib?

[Ruben Van de Velde]

Yeah, that issue is about when you want to compile a program that uses mathlib. I think you're just hitting the issue that mathlib is quite big. You can start by importing specific modules that look relevant

[tau]

I'm not really proficient with Lean, currently taking courses on formal verification in my uni. I'm still not sure which tactics come from Lean and which from Mathlib, considering there are some that come from both (e.g. apply x comes from Lean, but apply x at y from Mathlib IIRC). So figuring out which modules I need to import might take even more time than trying to prove a theorem.

[Damiano Testa]

If you use import Mathlib.Tactic you get a good selection of math results and all (most?) mathlib tactics.

[Bryan Gin-ge Chen]

It requires you to have a compiling file first so I don't know if it will work for your current issue, but there's also the #min_imports command which will tell you what the minimum imports you need are.