Running lean on an external SSD

Stream: lean4

[Dhyan Aranha]

My disk space on my personal computer is getting filled really quickly with lean projects so I recently bought an external drive to put all my lean projects on. However when I try to work on the files on the external drive I've never even managed to get lean to start running, the info-view just sort of hangs forever. I was wondering if I am missing something obvious? (when I ask gemini I get into long discussions about olean files etc...)

[Arthur Paulino]

I've never tried this, but I think informing your operating system is important here

[Shreyas Srinivas]

I'd recommend keeping a local lean install and moving projects to the SSD

[Dhyan Aranha]

In what sense do you mean "informing"?

[Shreyas Srinivas]

As long as the disk and your machine have the same filesystem, things should be fine

[Dhyan Aranha]

I think everything has the same file system. I'm running Mac OS and I configured my external hard disk to APFS

[Henrik Böving]

Shreyas Srinivas said:

As long as the disk and your machine have the same filesystem, things should be fine

That doesn't matter at all.

Dhyan Aranha said:

My disk space on my personal computer is getting filled really quickly with lean projects so I recently bought an external drive to put all my lean projects on. However when I try to work on the files on the external drive I've never even managed to get lean to start running, the info-view just sort of hangs forever. I was wondering if I am missing something obvious? (when I ask gemini I get into long discussions about olean files etc...)

Can you at least get the projects to work from the CLI? So for example run lake build manually in them?

[Floris van Doorn]

Not your question, but to clear up disk space, feel free to

• delete the .lake folder in old projects
• delete old/all cache files in ~/.cache/mathlib
• delete old/all toolchains in ~/.elan/toolchains (in this case, I'm not sure if it's important to also delete the corresponding ~/.elan/update-hashes)

Lean will redownload these things when you need it again.

[Kevin Buzzard]

Don't know if this is the issue but when I tried this, it turned out that my external SSD had far slower r/w speed, so the part of lake exe cache get where Lean decompressed 7000 files would sometimes take many minutes, giving the impression that something had hung. What I do now is that I store many barely-used projects on my SSD (where I have lots of space so don't need to delete .lake and which I occasionally run but never bump) and I leave the two projects which I work mostly on (mathlib and FLT), and where I am constantly updating oleans, on my hard drive (which is much quicker for r/w operations).

[Dhyan Aranha]

Henrik Böving said:

Can you at least get the projects to work from the CLI? So for example run `lake build` manually in them?

When I run lake build I get the message: "Build completed successfully", but the little circle in the info-view just turns forever.

@Floris van Doorn , @Kevin Buzzard Thanks for the tips!

[Julian Berman]

A second piece of advice might be to set the $MATHLIB_CACHE_DIR environment variable, or arguably the $XDG_CACHE_DIR variable entirely, to be a directory on your larger disk. But this also won't solve your current problem -- to be clear, if you just create a single empty file on the external drive with no imports and you open it and put #check 37 in it, you get nothing in your infoview?

[Shreyas Srinivas]

Henrik Böving said:

Shreyas Srinivas said:

As long as the disk and your machine have the same filesystem, things should be fine

That doesn't matter at all.

Fair enough. This is just my setup where things work fine. So it's a sufficient set of conditions to make things work. Maybe not necessary ones.

[Dhyan Aranha]

Julian Berman said:

A second piece of advice might be to set the $MATHLIB_CACHE_DIR environment variable, or arguably the $XDG_CACHE_DIR variable entirely, to be a directory on your larger disk. But this also won't solve your current problem -- to be clear, if you just create a single empty file on the external drive with no imports and you open it and put #check 37 in it, you get nothing in your infoview?

Hey Julian! Yeah that's correct, I just made a new lean file with no imports and in the info view it says "no info found"

[Julian Berman]

Hmmm interesting. I don't have any immediate ideas honestly. If you click on the buttons in the forall menu when you have a file on the external drive open:

Screenshot 2026-02-19 at 18.21.06.png

Specifically the "show troubleshooting output" and "show setup information" ones, do either have anything interesting looking in them?

[Julian Berman]

And, I know you said you are on macOS so I assume not, but just to check, you don't have any endpoint "security" malware installed do you? JAMF, some other university related thing posing as antivirus, etc. etc.?