disc space and .cache remark

Stream: mathlib4

[Kevin Buzzard]

I ran out of disc space yesterday and the reason was that I had 145 gigs in \~/.cache/mathlib; this turned out to be 2.4 million files called things like 8521368773646758302.tar.gz and 55c0087019cbc8cd.ltar; it was not completely trivial to even delete them because rm *.ltar gave me a bash error /usr/bin/rm: Argument list too long :-)

[Henrik Böving]

rm -rf 1*.ltar and work your way through hex !

[Kevin Buzzard]

buzzard@brutus:~/.cache/mathlib$ rm 1*.ltar
bash: /usr/bin/rm: Argument list too long
buzzard@brutus:~/.cache/mathlib$ rm 11*.ltar
buzzard@brutus:~/.cache/mathlib$

but rm 0[01234]*.ltar was OK. Took me a while! The machine is from 2019 or so (and has been used to do little else but Lean since then).

[Kevin Buzzard]

I might be imagining it but my impression is that the "Decompressing/Unpacked" part at the end of lake exe cache get is now much much quicker on this machine.

[Bryan Gin-ge Chen]

We had to add a step to our CI a while back because of the same problem. I guess we want some kind of auto-cleanup for users as well in Cache?

[Louis Cabarion]

This gets around the Argument list too long issue:

% find .cache/mathlib/ -type f -name "*.ltar" -exec rm {} \;

If you want to do a "dry run" first:

% find .cache/mathlib/ -type f -name "*.ltar" -exec ls -dl {} \;

[Kim Morrison]

Doesn't just rm -rf .cache/mathlib also suffice?

[Kevin Buzzard]

I was scared about removing the stuff which wasn't .ltar files! (loads of versions of leantar)

[Violeta Hernández]

I've been hovering around 10 gigs left for the past few months. A tool to clear the cache every once in a while would be quite appreciated!