lean projects taking a lot of hdd space

Stream: new members

[Rado Kirov]

Every math lean project I am working on takes 6GB because of mathlib and ~/.elan is 20GB because of old versions of the lean toolchain, that projects might or might not need. So I am slowly running out of diskspace on my M2. How do other folks manage this (other than work on fewer lean math projects)?

Mathlib will surely grow 2x in 1-2 years, and I am not sure hdd manifacturers can keep up :)

[Philippe Duchon]

Is there a good reason to set up multiple Lean projects when just playing around? I tend to have things I try to prove, on various largely unrelated topics, and at the moment I just have a single project and any number of unrelated files in there. I don't have particular requirements (if I find out my version of Mathlib is sufficiently out of date that I don't have access to some theorems that I read about in the online documentation, I'll simply update).

I suppose multiple projects become meaningful if you're collaborating with different people - especially if you're going to contribute to Mathlib - but I'm clearly not there yet; mostly, trying to learn by doing (i.e. exercises that were not set up for me by someone else).

[Henrik Böving]

Rado Kirov said:

Every math lean project I am working on takes 6GB because of mathlib and ~/.elan is 20GB because of old versions of the lean toolchain, that projects might or might not need. So I am slowly running out of diskspace on my M2. How do other folks manage this (other than work on fewer lean math projects)?

You can use elan toolchain gc to gc toolchains that are not used in any project on your machine anymore. Regarding the caches across multiple mathlib projects we hope to bring a solution for shared project caches in the near-ish future.

Mathlib will surely grow 2x in 1-2 years, and I am not sure hdd manifacturers can keep up :)

Terrabyte sized storage (I assume you are actually talking about SSDs and not HDDs here) is quite cheap nowadays, I would imagine mathlib can easily do at least 10x before we run into any issues.

[Ruben Van de Velde]

That said, it might be good if we could reduce the sizes a bit

[Anthony Wang]

If your disk is using a filesystem that can do deduplication such as btrfs or zfs, you might be able to use that to reduce disk usage of multiple identical copies of mathlib. I haven't tried that out to see if it would work though since I haven't had any problems yet with Lean using too much disk space.

[Kevin Buzzard]

I (a) sometimes delete ~/.cache/mathlib and (b) sometimes delete .lake in projects which I am not using regularly