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