Zulip Chat Archive

Stream: new members

Topic: Lean4 errors on MacOS


Marco Campos (Dec 15 2023 at 06:04):

Greetings,
I played with Lean4 a while ago when it first came out but I haven't been able to get it working on mac again. My elan version is 3.0.0 and when I try to use elan self update, I get the errors:

error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

I haven't been able to find many solutions for this, any suggestions on what to try?

For some additional context, if I try to initialize a LEAN project, I get the following error:

Warning: recommended `curl` version 7.81. Found 7.78.0
Attempting to download 3902 file(s)
Downloaded: 0 file(s) [attempted 3902/3902 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress

Yaël Dillies (Dec 15 2023 at 07:16):

On MacOS, you should use brew to update elan.


Last updated: Dec 20 2023 at 11:08 UTC