One Mathlib to rule them all?

Stream: general

[Yitzhak Zangi]

Since I started to learn lean, I cloned several lean repositories to do lean exercises (like MIL etc.), however, in the last few days, when I tried to install some software to may laptop (win11, almost 440GB) I was informed that I don't have enough space, and upon inspection I noticed that the lean + .lake directories are over 40GB!
Is there a way to reduce used space by maintaining only one copy of mathlib? I remember that @Kim Morrison said something about that months ago that involve the new module system, but

• I haven't found the conversation, and
• I don't see how this will reduce the space.

So is there a way to reduce (pretty urgently) the space used by lean, other than to delete some directories?

[Chris Bailey]

There were some community notes put here and there was a suggestion in passing that one could specify (in each dependent project) the mathlib dependency by using a local path pointing to the shared mathlib, but I think all of these suffer from (at least) the same weakness of requiring the dependent packages to use the exact same version of mathlib.

[Jon Eugster]

https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation

Here are my thoughts about it. However, note that the process described there is quite a manual one, and I can't really recommend it.

The easier solution might be to just delete stuff you don't need anymore or get an external drive...

[Jakub Nowak]

You could try using filesystem with automatic deduplication too. But that's also not easy to setup, if you're not already on zfs or btrfs.

[Kevin Buzzard]

If it's urgent then a short-term practical solution is to either delete directories in $HOME/.elan/toolchains corresponding to old versions of lean (each deletion saves about 2-2.5 gigs), or to delete .lake directories in individual projects (if they depend on mathlib then such a deletion could save 8 gigs). Any such deletion can be easily reversed with lake exe cache get in the relevant repo if you want the project running again; the relevant data will be downloaded in under a minute(*).

[Ruben Van de Velde]

(*) your download speed may vary