How to save .cache folder in some other directory?

Stream: general

[Robert Joseph]

Hey I was just wondering when you compile a lean project and it stores say the mathlib data in .cache, is there any way to force it to save it in some other directory? Reason is that when I am working on these clusters, on my home directory the cache takes a huge amount of space and would like to move it to pscratch or raid where there's like way more space!

[Eric Wieser]

You could symlink .cache/mathlib to where you actually want it to go

[Robert Joseph]

Oh I see, is there any other way? like exporting or setting up a path to store it somewhere else. Same for elan! https://github.com/leanprover/elan like it tells me that I can choose which path to install, but when I have to modify the path variable during installation, it only lets me do a y/n answer and not specify the path? so how can I also ensure I don't install elan on my home but rather in the raid directory
image.png

[Julian Berman]

MATHLIB_CACHE_DIR is the envvar you're looking for

[Julian Berman]

E.g. https://github.com/Julian/dotfiles/blob/main/.config/zsh/.zshenv#L81

[Julian Berman]

ELAN_HOME for elan

[Robert Joseph]

omg thank you so much! this has been a lifesaver