Cleaning caches

Stream: general

[Yaël Dillies]

Is there a proper way to get rid of outdated caches on one's machine? I can delete them all but I wondered whether there was a more civilized way.

[Yaël Dillies]

Here are mathlib's caches on my computer. I took the picture using WinDirStat. 14GB!

[Scott Morrison]

Delete ~/.mathlib whenever you like.

[Kevin Buzzard]

leanproject get-cache will just happily redownload any which you find that you need again (eg caches of mathlib commits used in other projects).

A warning though -- you might also have a bunch of old lean binaries for old versions of lean (eg I still have nightlies from 2018 on my machine) and here it's more complicated -- there are two directories to delete per cache IIRC and I think elan gets quite confused if you only delete one of them