Is there a way to include only part of Mathlib?

Stream: Is there code for X?

[Shin Gen]

The .olean's of Mathlib itself, along with its dependencies is more than 6GB, which is almost unacceptable in my scenario. However I only require a small part of Mathlib, and many of the imports can be well stripped. (Why would I ever need these linters defined in Mathlib.Init, especially at runtime? Plus, as long as proof bodies are ignored while building oleans, the imports of Mathlib.Tactic is most of the times useless.) Therefore, I believe including just part of Mathlib (for example only the Data part) in the project is feasible and can save me a lot of space, but I wonder if there is already a solution for this?

[Eric Rodriguez]

the module system in 4.25 is aiming to address this somewhat

[Shin Gen]

Ah, I haven't found a changelog of Mathlib but it's relieving to hear that it is adopting a module system.

[Kim Morrison]

@Shin Gen, you might have to clarify what you mean by "include".

• You don't have to import Mathlib, you can just import Mathlib.Foo.Bar, or whatever you need.
• You don't need to download the entire cache, you can run lake exe cache get Mathlib.Foo.Bar to only retrieve parts of it.

(and the module system will enable "including" even less, as noted above).

[Shin Gen]

"You don't need to download the entire cache" that's what I actually mean, thank you.