Old `.tar.xz` files

Stream: general

[Stuart Presnell]

I've just found that I have 200 old .tar.xz files in my /Users/stuartpresnell/.mathlib/folder, downloaded each time I run leanproject --debug up and totalling almost 12 GB. I assume it's safe to delete these — (I hope it is, because I've already deleted them before thinking to ask about it! :confounded:)

[Patrick Massot]

It's perfectly safe. Worst case if you'll need to redownload them.

[Stuart Presnell]

Thanks! Is there any way to have leanproject automatically delete the old files?

[Patrick Massot]

leanproject currently doesn't have that feature, but if this is important to you then you can implement it and open a pull request. There is no obstruction, it's simply that nobody ever felt it was important enough to take time to do it.