Zulip Chat Archive
Stream: new members
Topic: customize lean directory
Hank (Dec 16 2021 at 07:43):
Hello! I am following this website to download lean: https://leanprover-community.github.io/install/windows.html.
After running the curl https... command, I get the message saying that
It will add the leanpkg, lean, and elan commands to Elan's bin directory, located at: C:\Users\user\.elan\bin.
Can I change the directory to another hard drive like D or E?
Eric Wieser (Dec 16 2021 at 09:15):
Does D:\Users\user exist for you?
Eric Wieser (Dec 16 2021 at 09:17):
Or perhaps a better question; what does echo %homedrive%%homepath% give on your system?
Hank (Dec 17 2021 at 01:38):
C:\Users\user
Oh should I change my homedrive homepath settings then?
Eric Wieser (Dec 17 2021 at 01:48):
Not unless you know what you're doing
Eric Wieser (Dec 17 2021 at 01:49):
Why do you want to move where elan installs to?
Hank (Dec 17 2021 at 01:50):
because my c drive is full
Eric Wieser (Dec 17 2021 at 01:52):
Regarding moving your home directory: https://www.zdnet.com/article/dont-move-your-windows-user-profiles-folder-to-another-drive/?_amp_linker=1*1kj3vb8*id*bnN3M1pjWlBTQ2UwRDdpeW9ONVpTZXBGRlpRXzl3VVVydWNrR0dQV3UzSFlaLVpnNGRhc0NLMUtTbmtfY2Jmdw..#ftag=CAD-00-10aag7e
Eric Wieser (Dec 17 2021 at 01:53):
Microsoft does not recommend that you change the location of the user profile directories or program data folders
Eric Wieser (Dec 17 2021 at 01:53):
Can I suggest you move something else off your C drive to make room?
Hank (Dec 17 2021 at 01:56):
ok yeah thats less dangerous
Kevin Buzzard (Dec 17 2021 at 09:35):
elan is tiny!
Eric Taucher (Dec 17 2021 at 09:57):
Hank said:
because my c drive is full
My sword of choice for identifying what to remove or move on a near full Windows drive:
WinDirStat is a disk usage statistics viewer and cleanup tool for various versions of Microsoft Windows.
Note: if you are looking for an alternative for Linux, you are looking for KDirStat (apt-get install kdirstat or apt-get install k4dirstat on Debian-derivatives) or QDirStat and for MacOS X it would be Disk Inventory X or GrandPerspective.
Yaël Dillies (Dec 17 2021 at 09:58):
Yeah, can only heartwarmingly recommend WinDirStat myself. That's how I found out how much storage mathlib caches were taking.
Jireh Loreaux (Dec 17 2021 at 18:09):
Of course, there's always du -sh * for diagnosing large disk usage issues quickly.
Last updated: Dec 20 2023 at 11:08 UTC