Zulip Chat Archive

Stream: new members

Topic: M1 macs

Jake Levinson (Feb 23 2021 at 01:44):

Hi all,

I just tried to install Lean after playing through the Natural Number Game, which I came across on hackernews yesterday. Compliments to Kevin and Mohammad for a very convincing introduction! (speaking as a mathematician here :smile:)

I'm on a recently-acquired M1 mac and was not able to install elan through the instructions at https://leanprover-community.github.io/get_started.html.

Error message: elan: unknown CPU type: arm64
(brew and leanproject installed just fine)

I am technically ignorant about M1 stuff and haven't yet had to use Rosetta for anything, so I'm not sure how to fix this or what to do instead. I saw some discussion up above about getting Lean to work on an M1 mac, but don't understand it. Anyone willing to help a newbie get set up?

Thanks!
-JL

Bryan Gin-ge Chen (Feb 23 2021 at 01:53):

Welcome! I think the issue is that elan does not have binaries for arm64 (yet?). Are M1 macs able to run binaries for intel macs? If so, then maybe the apple-darwin file here will work: https://github.com/Kha/elan/releases/tag/v0.10.3

Bryan Gin-ge Chen (Feb 23 2021 at 01:55):

I haven't tried to install elan manually before, but the instructions say just to run the file in a terminal after unpacking it.

Jake Levinson (Feb 23 2021 at 02:11):

Hi Bryan, thank you! Some progress now -- that installer seems to have worked and successfully installed elan. I've cloned the Lean tutorials.

New error message: looks like something else hasn't installed correctly (maybe leanpkg?): VSCode appears to be running leanpkg configure and getting this error:

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib Referenced from: /Users/jake/.elan/toolchains/leanprover-community-lean-3.26.0/bin/lean Reason: image not found

Note -- I do have gmp installed already via brew install gmp.

Bryan Gin-ge Chen (Feb 23 2021 at 02:14):

Hmm, leanpkg is just a .lean script, so I think lean is not able to find gmp for some reason.

Bryan Gin-ge Chen (Feb 23 2021 at 02:16):

Is it possible that the gmp you got from homebrew is an arm64 version and not compatible with a program compiled for an intel mac? (I have no idea, just guessing wildly...)

Julian Berman (Feb 23 2021 at 02:17):

That'll be it yeah, paths to ARM things from homebrew will be in /opt/

Julian Berman (Feb 23 2021 at 02:22):

you can install an intel homebrew as well and then it'll get you an intel libgmp if you use that one instead, or you can also reasonably easily compile lean natively for ARM, there's just one cmake arg you need which is https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Apple.20Silicon/near/219305416

Bryan Gin-ge Chen (Feb 23 2021 at 02:34):

I suspect the former route might be easier for a new user; otherwise, if you want leanproject to work then you'll have to make sure you compile Lean at the correct v3.26.0 commit and then recompile when we upgrade mathlib to a new version.

Jake Levinson (Feb 23 2021 at 04:22):

Update:

Your suggestions worked -- recording for posterity here in case anyone else reads this: it turned out I actually already had intel homebrew installed as well (presumably because my current macbook copied everything from my previous macbook automatically when I was first setting it up).

But, I had to actually call that version of homebrew directly to install x86 gmp, that is /usr/local/Homebrew/bin/brew install gmp instead of brew install gmp even though the command ran in a Rosetta terminal... I guess this makes sense but wasn't obvious to me at first!

And after fiddling a bit more, I appear to have the tutorials up and running in VSCode!

Thanks Bryan and Julian!

goals accomplished :tada:

Kevin Buzzard (Feb 23 2021 at 08:01):

Oh boy, thanks for persevering!

Bryan Gin-ge Chen (Feb 23 2021 at 16:56):

@Jake Levinson Glad you got things working! If you don't mind, can you try and recall all the steps you took so we can add some M1-specific instructions to our webpage?

Jake Levinson (Feb 23 2021 at 17:35):

This is going to be messy, haha. Maybe I should reinstall it all (homebrew, elan, lean, etc) from scratch now that I know how to get it working. The actual sequence involved a bunch of no doubt superfluous steps.

What I actually did was:

  1. (I had homebrew and git already installed in both intel and arm64 versions, though I didn't realize I had both copies at first).

  2. I ran the install command from [https://leanprover-community.github.io/install/macos.html] in Terminal:
    /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

  3. I followed these instructions [https://osxdaily.com/2020/11/18/how-run-homebrew-x86-terminal-apple-silicon-mac/] to make a duplicate Terminal that would run using Rosetta.

  4. I basically now reran a bunch of installers both terminals. Homebrew; the install command from Step 1; Bryan's suggested package for elan; VSCode; brew install gmp and brew install coreutils. (Some of these installers automatically declined to make a second copy of their installation.)

At this point I was able to copy the tutorial using leanproject get tutorials. When I opened it in VSCode, it caused a bunch of "memory capacity exceeded" errors in the VSCode Infoview (I forget the exact error message, unfortunately). This stopped happening once I ran leanproject build tutorials. I'm not sure if that was supposed to be necessary.

Still, lean was still not functional because it couldn't detect gmp.

  1. Finally I forced Homebrew to install the x86 gmp using Julian's suggestion. Specifically I went and found the intel Homebrew installed in /usr/local/Homebrew and ran the gmp installer with it as /usr/local/Homebrew/bin/brew install gmp instead of brew install gmp. (The latter command had been, I think, invoking arm64 Homebrew even if I ran it in the Rosetta Terminal.)

That seemed to do it!

(edit: Oh, there was more too. I think I ran some other commands like pipx ensurepath and maybe related stuff in both terminals. Basically I was trying to do all the steps from https://leanprover-community.github.io/install/macos_details.html.)

If I have time this weekend I'll delete it all and try a fresh install.

Bryan Gin-ge Chen (Feb 23 2021 at 17:40):

Thanks Jake! This is already really helpful!

Bryan Gin-ge Chen (Feb 23 2021 at 17:41):

I believe leanproject get tutorials should've made it unnecessary to run leanproject build tutorials, as one of the things it does is to download the compiled files for the version of mathlib used in the tutorials. Not sure if the lack of gmp somehow caused Lean to be unable to find them.

Scott Morrison (Sep 08 2021 at 23:35):

@Ania Misiorek, now that you've changed the thread title, do you see the message above from Jake Levison? He describes the steps in his successful installation on an M1 mac.

Scott Morrison (Sep 08 2021 at 23:35):

It would be helpful to also have your report of either a successful recipe, or failure points.

Scott Morrison (Sep 08 2021 at 23:36):

Unfortunately not many of us have M1 macs yet!

Justin Pearson (Sep 09 2021 at 05:47):

I just compiled lean3 from the source on my M1 Mac. elan does not yet (last time I checked) work on M1 Macs. The downside of compiling from source, is that you have git checkout release rather than the latest git commit. The latest git commit could be a bit too experimental. After that everything just works, but you don't get elan support for different versions of lean.

Justin Pearson (Sep 09 2021 at 05:51):

I forgot to say, you also have to install leanproject yourself via pipx. If you haven't used your mac for development then you will have to set a quite a few things such as homebrew, and installing the xcode command line tools.

Marcus Rossel (Sep 09 2021 at 08:14):

I'm not sure of the steps I took anymore, but I use elan on an M1 Mac.

Marcus Rossel (Sep 09 2021 at 08:14):

I think it involved using homebrew.

Marcus Rossel (Sep 09 2021 at 08:16):

There's a thread called "Lean 4 on M1 Macs" in which this is discussed.

Julian Berman (Sep 09 2021 at 16:58):

@Marcus Rossel Perhaps you're using intel homebrew (and therefore rosetta'd lean)? file =lean and/or file =elan should tell you (or feel free to share the output), it'll say at the end Mach-O 64-bit executable arm64 if it's arm64, but yeah elan isn't going to give you those.

Also I've tried to update most of the docs for this that I could find, but I'm pretty sure there's at least 1 PR still unmerged updating instructions (and then 1 ticket for making things "automatically work" as best they can). Certainly help is still welcome.

Julian Berman (Sep 09 2021 at 16:59):

@Justin Pearson

The downside of compiling from source, is that you have git checkout release rather than the latest git commit.

Yes definitely -- I think Brian mentioned this above in this thread, but if you don't get this commit right, you'll also find that oleans that leanproject downloads will not work on your lean (or really, they'll not be useful, and your lean will recompile things).

Julian Berman (Sep 09 2021 at 17:01):

I forgot to say, you also have to install leanproject yourself via pipx.

This is the outstanding PR that needs merging to update the docs -- pipx isn't necessary anymore, brew install mathlibtools will give you a working leanproject even on M1s.

I'll ping someone on that PR (https://github.com/leanprover-community/leanprover-community.github.io/pull/194) to see if we can get it merged).

Hector Padilla (Sep 10 2021 at 20:22):

I managed to install elan on my M1 Mac as well as the lean extension, but I get this error in VS Code: server has stopped due to signal SIGABRT

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
Referenced from: /Users/hec/.elan/toolchains/stable/bin/lean
Reason: image not found

Julian Berman (Sep 10 2021 at 20:36):

Hi! Can you:

  • show the output of file /Users/hec/.elan/toolchains/stable/bin/lean
  • same for otool -L /Users/hec/.elan/toolchains/stable/bin/lean
  • explain briefly what you ran to get elan, and then what you did to get lean, and how you got vscode

If you want to interpret that error -- it's saying "the dynamic linker can't find libgmp", or even simpler "lean can't find a dependency of itself while it's trying to start". And I can see from the path it's looking in that is trying to find an intel libgmp (which is going to live in /usr/local/opt). If you share a bit more about what you ran it'll likely help.

Hector Padilla (Sep 10 2021 at 20:59):

Thank you! When I run, file /Users/hec/.elan/toolchains/stable/bin/lean

/Users/hec/.elan/toolchains/stable/bin/lean: Mach-O 64-bit executable x86_64

And when I run, otool -L /Users/hec/.elan/toolchains/stable/bin/lean

/usr/local/opt/gmp/lib/libgmp.10.dylib (compatibility version 15.0.0, current version 15.1.0)
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1292.60.1)
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 904.4.0)

I used Jake's method above to install elan. I also installed lean extension through vscode and installed vscode through their website.

Julian Berman (Sep 10 2021 at 21:02):

OK cool, so you have a fully intel lean and elan at least. Does ls /usr/local/opt/gmp/lib show that that exists (and contains that file)?

Hector Padilla (Sep 10 2021 at 21:03):

it says no such file or directory exists

Julian Berman (Sep 10 2021 at 21:05):

Aha, interesting ok. Can you try re-running /usr/local/Homebrew/bin/brew install gmp and let me know what it does?

Hector Padilla (Sep 10 2021 at 21:19):

Warning: No available formula or cask with the name "gmp".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.

Julian Berman (Sep 10 2021 at 21:25):

Hrm, interesting... And if you run /usr/local/Homebrew/bin/brew update and then try it again?

Jake Levinson (Sep 11 2021 at 01:18):

One possibly relevant fact about my approach earlier this year: at some point, the Rosetta terminal I created stopped working. Unfortunately, it was a while ago (maybe around the start of the summer?) and I don't remember exactly what was wrong with it. But, either way, Lean and VS Code were working for me at that point (and still is), so I didn't question it...

Justus Springer (Sep 21 2021 at 14:48):

I found this thread as I'm considering buying an M1 mac. Besides the installation issues (which make me feel a little intimidated), is the M1 a good machine for lean? On my 5-year-old windows notebook, Lean can be pretty slow at times, which is one of the reasons I'm thinking of buying a new notebook.

Trevor Fancher (Sep 21 2021 at 14:59):

My M1 MacBook Air handles Lean like a champ. Installation was a pain, but I've mostly got it figured out. I built elan from source and then let it pull whatever lean binaries it wants (usually from a call to leanproject). They will be x86 binaries and they will fail to run. So then I go intro elan's folder and overwrite them with the proper version of lean that I manually build from source. Then everything works. I can explain in more detail if anyone is interested. The benefit of this hack is that leanproject works.

Justin Pearson (Sep 21 2021 at 15:30):

If you are happy with only having one version of lean, then it seems that you don't really need elan. I tend to use "leanproject --no-lean-upgrade upgrade-mathlib" The real problem with the M1 macs is that even though you have the intel emulation , mixing it with native M1 binaries is a bit of a mess, so it takes some planning.

Bryan Gin-ge Chen (Sep 21 2021 at 15:45):

Trevor Fancher said:

My M1 MacBook Air handles Lean like a champ. Installation was a pain, but I've mostly got it figured out. I built elan from source and then let it pull whatever lean binaries it wants (usually from a call to leanproject). They will be x86 binaries and they will fail to run. So then I go intro elan's folder and overwrite them with the proper version of lean that I manually build from source. Then everything works. I can explain in more detail if anyone is interested. The benefit of this hack is that leanproject works.

Yes, detailed instructions in this thread would definitely be helpful for others, particularly as we don't have much on M1 Macs on our website right now!

Justus Springer (Sep 21 2021 at 15:49):

Thanks for the info! I hope my excitement of looking forward to a fast lean environment will mitigate the installation pain.

Trevor Fancher (Sep 21 2021 at 16:19):

@Bryan Gin-ge Chen I'll write something up and post it back here. There are a bunch of steps, so it may take a day or so before I have time to remember/rediscover the process.

Trevor Fancher (Sep 22 2021 at 00:42):

@Bryan Gin-ge Chen I went ahead and put the instruction in a new thread #new members > M1 Macs: Installing the Lean 3 toolchain . I forgot just how convoluted the whole process is. It really does work, though :)

Bryan Gin-ge Chen (Sep 22 2021 at 00:53):

Thanks! I've taken the liberty of editing the title to explicitly say "Lean 3".

Bryan Gin-ge Chen (Sep 22 2021 at 00:53):

Oops, I guess that broke the link in your message. Sorry!

Trevor Fancher (Sep 22 2021 at 00:54):

No problem, I fixed it :)

Hector Padilla (Oct 25 2021 at 15:44):

Hey I'm still getting this SIGABRT error, does anyone know how to fix it? I tried restarting lean. I am also running on a M1 mac. Screen-Shot-2021-10-25-at-11.43.33-AM.png

Eric Rodriguez (Oct 29 2021 at 10:17):

I'm thinking about trying to get one of the new macbooks (which I'm not too happy about, but by all reports this M1 Pro is an absolute beast...). Has anyone tried Lean on one of then yet?

Jason Rute (Oct 29 2021 at 11:29):

@Eric Rodriguez A few people have (both with Rosetta and installing natively). Besides this thread, search Zulip for "apple silicon", "M1", "aarch64" and "arm". I don't have one yet. (I was going to buy one, but then my old company offered me my work MacBook Pro for $200 when I left.) However, the impression I get is that it works well and is fast (even on the M1 MacBook Air, both emulated on Rosetta or installed natively), but if you are going to install it natively you currently have to compile from source which is some additional work. Instructions are at #new members > M1 Macs: Installing the Lean 3 toolchain (There is some discussion in #general > Apple Silicon about making an M1 binary to make installation easier, but it involves changes to the current GitHub workflow.)

Jason Rute (Oct 29 2021 at 11:42):

Sorry, maybe I misunderstood. Were you asking specifically about running Lean on a new M1 Pro/Max chip to get a sense of the performance? (Given the good reviews for the early M1 chip, I'm sure it's great, but I'd also love to hear from folks how great.)

Eric Rodriguez (Oct 29 2021 at 13:12):

Yes, although this is also very useful info! If I end up getting it, I'll report back :)

Nick Yu (Feb 09 2022 at 10:59):

@Hector Padilla Maybe check if gmp got installed in /usr/local/Homebrew/opt when using intel homebrew, in my case it got installed in the homebrew opt directory.

Not the best solution, but you can change the referenced shared library with install_name_tool -change /usr/local/opt/gmp/lib/libgmp.10.dylib /usr/local/Homebrew/opt/gmp/lib/libgmp.10.dylib /Users/hec/.elan/toolchains/stable/bin/lean.

Cris Perdue (Mar 22 2022 at 03:59):

Nick Yu said:

Hector Padilla Maybe check if gmp got installed in /usr/local/Homebrew/opt when using intel homebrew, in my case it got installed in the homebrew opt directory.

Not the best solution, but you can change the referenced shared library with install_name_tool -change /usr/local/opt/gmp/lib/libgmp.10.dylib /usr/local/Homebrew/opt/gmp/lib/libgmp.10.dylib /Users/hec/.elan/toolchains/stable/bin/lean.

In the end I completed the install using homebrew as described at https://leanprover-community.github.io/install/macos.html. But this put Lean at $HOME/.elan/toolchains/leanprover-community--lean---3.41.0/bin/lean. So the command to fix the reference to libgmp had to point to there.

Jujian Zhang (Mar 23 2022 at 15:20):

Recently there is an alpha release for asahilinux which is specifically made for apple M1 chips. Their is a super easy to use installer scripts. I just get Lean run locally on this Linux distro. The only problem is that visual studio code doesn’t work; so one has to use code-server which is like visual studio code but with user interface in a browser.

Eric Rodriguez (Mar 23 2022 at 15:41):

Ooh, can you send a link? How come code doesn't work?

Jujian Zhang (Mar 23 2022 at 16:53):

https://asahilinux.org

Jujian Zhang (Mar 23 2022 at 16:53):

All lean code works; it’s just visual studio code the editor doesn’t compile.

Jujian Zhang (Mar 23 2022 at 16:55):

https://github.com/coder/code-server
This link is vscode in browser

Daniel Ever (Oct 15 2022 at 00:00):

Good day to everyone! Recently I've found some more time to dive into Lean once again, but currently have problems while installing Lean on my M1 Mac Mini. I've carefully followed the steps provided here: https://leanprover-community.github.io/install/macos.html, everything looked fine, but in the end after I've downloaded Mathematics_in_lean using leanproject getall the commands are highlighted by the red lines.

the explanation is "file 'data/real/basic' not found in the search path" and so on. I'd be grateful if someone could direct me to what to do next since I'm not really familiar with programming, Visual Studio and other IT-related subjects. Thanks in advance!

Matt Diamond (Oct 15 2022 at 03:03):

Are you using VSCode? If so, do you see leanpkg.toml and leanpkg.path at the root of the open directory?

Kevin Buzzard (Oct 15 2022 at 07:04):

Yeah, often the issue is that the user did not open the root directory of a lean project with VS Code's "open folder" functionality

Daniel Ever (Oct 15 2022 at 11:08):

Matt Diamond said:

Are you using VSCode? If so, do you see leanpkg.toml and leanpkg.path at the root of the open directory?

indeed, it solved the issue! I never thought it was important since I was already insider the folder and used code command to get there before. Thanks for your help!

Dhruv Bhatia (Dec 31 2022 at 17:48):

Hello! I got a new m1 mac recently and have wanted to install lean. I've been following the instructions on https://leanprover-community.github.io/install/macos.html, but get stuck at the part where I run the command arch -x86_64 zsh. It keeps giving me the error arch: posix_spawnp: zsh: Bad CPU type in executable. I don't really have much familiarity with how these things work, so would appreciate any help!

Marcus Rossel (Jan 01 2023 at 13:37):

@Dhruv Bhatia You probably haven't installed Rosetta yet: https://apple.stackexchange.com/a/408379/119179

Bolton Bailey (Jan 02 2023 at 08:12):

@Marcus Rossel Note that this was the error message a friend of mine got after Rosetta 2 installed apparently successfully. Do you think it really is that Rosetta is corrupted as was commented in that part of the thread, and if so, do you have a better fix than the pretty wild instructions I got on reinstalling it?

Marcus Rossel (Jan 02 2023 at 08:24):

@Bolton Bailey Unfortunately I'm not well-versed in this kind of topic either, but the next best thing I'd try is running the commands from a terminal that was explicitly launched using Rosetta: https://apple.stackexchange.com/a/428769

Dhruv Bhatia (Jan 02 2023 at 22:48):

@Marcus Rossel that worked! Thanks, I'd been banging my head against a wall for a while there!

Topo_Space (Jan 21 2023 at 19:24):

(deleted)

Topo_Space (Jan 22 2023 at 15:32):

Does somebody know what's the issue?

file 'topology/basic' not found in the search path Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

and when I check the lean --path it shows the following:
lean --path { "is_user_leanpkg_path": false, "leanpkg_path_file": "/Users/max/Local Repository/Lean/my_project/leanpkg.path", "path": [ "/Users/max/.elan/toolchains/leanprover-community--lean---3.50.3/bin/../library", "/Users/max/.elan/toolchains/leanprover-community--lean---3.50.3/bin/../lib/lean/library", "/Users/max/Local Repository/Lean/my_project/_target/deps/mathlib/src", "/Users/max/Local Repository/Lean/my_project/./src" ] }

Riccardo Brasca (Jan 22 2023 at 15:51):

I don't use a mac, but have you opened in VS code the folder you want to work in (and not only a single file)?

Topo_Space (Jan 22 2023 at 16:03):

yes I did

Topo_Space (Jan 22 2023 at 16:28):

Riccardo Brasca said:

I don't use a mac, but have you opened in VS code the folder you want to work in (and not only a single file)?

only the project must be opened with vscode. thanks for your mention. problem solved.

Bjørn Kjos-Hanssen (Jan 29 2023 at 18:32):

To try to resurrect this thread, I followed the instructions at https://leanprover-community.github.io/install/macos.html and it seemed to go okay. But in VS Code I'm just stuck on "parsing at line 1". (I did open a folder instead of a file so I'm at a loss at this point.)

Kevin Buzzard (Jan 29 2023 at 22:42):

Lean 3 or lean 4? Can you send a screenshot of your VS Code?

Bjørn Kjos-Hanssen (Jan 30 2023 at 22:06):

@Kevin Buzzard Lean 3. Here's a screenshot, but the "parsing at line 1" is hover text, so it disappears when I go to the screenshot app. Screen-Shot-2023-01-30-at-12.05.09-PM.png

Kevin Buzzard (Jan 30 2023 at 22:15):

That looks to me like you didn't open the root directory of your project using VS Code's "open folder" functionality. Can you send another screenshot with the file explorer open (or try and fix your problem by creating a correctly-formatted Lean project with a leanpkg.path and a leanpkg.toml in a root directory and all Lean files in a src directory, as would be created by leanproject new my_project?)

Bjørn Kjos-Hanssen (Jan 30 2023 at 22:22):

Thanks @Kevin Buzzard that did it! (Now I have side-by-side directories called my_project and my_playground which is probably not how it's supposed to look, but whatever...)

Topo_Space (Feb 03 2023 at 12:13):

since I have installed a separate brew for x86 based on this link, I have to manually enter /opt/homebrew/bin/brew when I want to install something on default brew directory. how to set default directory of brew?

Topo_Space (Feb 03 2023 at 12:30):

we can create alias for Intel brew: alias brew86='arch --x86_64 /usr/local/Homebrew/bin/brew'

Topo_Space (Feb 03 2023 at 12:30):

and add previous brew to path: path=('/opt/homebrew/bin' $path)

Jarod Alper (Feb 23 2023 at 01:36):

Hi all, I'm following the Lean installation instructions on https://leanprover-community.github.io/install/macos.html for an M1 Mac, and have run into some issues. 

==> elan-init
Bash completion has been installed to:
  /usr/local/etc/bash_completion.d
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.50.3
info: downloading component 'lean'
error: binary package was not provided for 'darwin'
info: using existing install for 'stable'
info: default toolchain set to 'stable'

  stable unchanged - Lean (version 3.42.1, commit 68455b087d87, Release)

Jarod Alper (Feb 23 2023 at 01:37):

When I run leanproject get ImperialCollegeLondon/formalising-mathematics-2022, it works! But leanproject get doesn't work for other lean repositories.

Adam Topaz (Feb 23 2023 at 01:56):

What's the error message with other repos?

Jarod Alper (Feb 23 2023 at 02:09):

info: downloading component 'lean'
error: binary package was not provided for 'darwin'
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

Adam Topaz (Feb 23 2023 at 02:21):

Aha okay. My guess is that the version of lean needed for the repo you're trying to fetch doesn't have a darwin binary for whatever reason.
Does leanproject get mathlib work?

Mauricio Collares (Feb 23 2023 at 02:52):

What's your elan version? You should update it if it's not 1.4.2.

Jarod Alper (Feb 25 2023 at 01:37):

Thanks for the suggestions! leanproject get mathlib also doesn't work. My elan version is 1.4.0 so that's likely the issue. I first tried redownloading elan but ended up installing an audio/video annotator (a different elan, i suppose). After realizing this, I tried elan self update which didn't work 

info: downloading self-update
error: failed to set permissions for '/Users/jarod/.elan/bin/elan-init'
info: caused by: No such file or directory (os error 2)

I tried downloading elan again but I got the error that I can't install elan with an existing lean installation. So perhaps I need to reinstall everything.

Julian Berman (Feb 25 2023 at 12:33):

@Jarod Alper what do ls -l ~/.elan/bin and ls -l ~/.elan say?

Anwoy Maitra (Feb 25 2023 at 15:09):

Hello. I'm a complete noob. I downloaded and installed Lean using the instructions available at
https://leanprover-community.github.io/install/windows.html
In particular, I installed GitBashPython and VS Code following the instructions. After that, I downloaded the tutorial project following the instructions available at
https://leanprover-community.github.io/install/project.html
I'm currently going through the tutorial project, and I haven't had too much mathematical trouble yet. I wanted to create a project of my own so that I could write Lean code just by myself and experiment (using some of the code snippets and exercises in Theorem Proving in Lean, which I'm reading). I tried to do that using the instructions available on the aforementioned web page. In particular, I ran the command
leanproject new proj1
inside Git Bash (which I had also downloaded when installing Lean). There was some output, but it contained an error message. The main error message seems to be "binary package was not provided for 'windows' ". In detail:

anwoy@anwoy-laptop MINGW64 ~/Dropbox/Work_tmp/Tmp
$ leanproject new proj1

cd proj1
git init -q
git checkout -b lean-3.42.1
Switched to a new branch 'lean-3.42.1'
configuring proj1 0.1
Adding mathlib
info: downloading component 'lean'
error: binary package was not provided for 'windows'
Command '['leanpkg', 'add', 'leanprover-community/mathlib']' returned non-zero exit status 1.

However, the folder "proj1" was indeed created. I opened that folder in VS Code and tried to create a ".lean" file. As soon as I did that, though, there was an error message, very similar to the one above. I'm attaching a screenshot for reference.

The strange thing is that I can work in the "tutorials" folder perfectly. None of the files in that folder show any errors, and I can even create ".lean" files of my own, and they are created error-free (I've done nothing on my own yet). Does anyone know what's going on and how this can be fixed? I would be very grateful for any help. If this is not the appropriate place to post this query, I apologize. I would be grateful if someone could direct me to the correct place.

Thanks in advance for any and all help! err_mssg.png

Julian Berman (Feb 25 2023 at 15:13):

@Anwoy Maitra welcome!-- this thread is technically about a particluar macOS-specific issue, but it sounds like you're on Windows. Zulip is a bit confusing to get used to, can you ask your question in a new thread with a title that's somewhat suitable to it?

Mauricio Collares (Feb 25 2023 at 15:28):

That being said, try running elan self update to see if it fixes your problem before asking in a new thread :)

Anwoy Maitra (Feb 25 2023 at 16:42):

Julian Berman said:

Anwoy Maitra welcome!-- this thread is technically about a particluar macOS-specific issue, but it sounds like you're on Windows. Zulip is a bit confusing to get used to, can you ask your question in a new thread with a title that's somewhat suitable to it?

Thank you very much for the detailed reply! Sorry for my stupidity; I just realized that the stream that I posted to is "new members / M1 macs". I'll repost my question in a thread with a title that sounds suited to it. Thanks again!

Anwoy Maitra (Feb 25 2023 at 16:44):

Mauricio Collares said:

That being said, try running elan self update to see if it fixes your problem before asking in a new thread :)

Thanks a lot for the suggestion! I'll do that before asking my question in a new thread.

Ella Yu (Jun 20 2023 at 09:40):

Hello! I am trying to install lean on my new M1 Mac. And I followed the instructions on https://leanprover-community.github.io/install/macos.html, but I get stuck at the part of running 'elan default stable' using brew (step 4). I keep getting the error : ("Failed to connect to github.com port 443 after 75526 ms: Couldn't connect to server") as the screenshot shown below. Thanks for your help!
Screenshot-2023-06-20-at-17.25.15.png

Kevin Buzzard (Jun 20 2023 at 09:41):

Are you behind a firewall? The error seems to indicate that you can't connect to github, but github seems to be working fine right now.

Kevin Buzzard (Jun 20 2023 at 09:42):

If I try connecting directly then the connection is established and then closed.

$ ssh -p 443 github.com
kex_exchange_identification: Connection closed by remote host
Connection closed by 140.82.121.3 port 443

But you're not even connecting.

Ella Yu (Jun 20 2023 at 09:43):

Kevin Buzzard said:

Are you behind a firewall? The error seems to indicate that you can't connect to github, but github seems to be working fine right now.

I can connect to GitHub using google chrome. but I am not sure why it doesn't work on my terminal.

Ella Yu (Jun 20 2023 at 09:45):

Kevin Buzzard said:

If I try connecting directly then the connetion is established and then closed.

$ ssh -p 443 github.com
kex_exchange_identification: Connection closed by remote host
Connection closed by 140.82.121.3 port 443

But you're not even connecting.

image.png
I got the same thing here.

Ella Yu (Jun 20 2023 at 10:08):

I think it works now. Thank you!

George Chemmala (Aug 05 2023 at 18:10):

I'm pretty new to Lean (and Zulip) so apologies for any naive mistakes. I'm getting an error with leanprojects when I try to build a lean 3 project:

info: downloading component 'lean'
error: binary package was not provided for 'darwin_aarch64'
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

I have gotten other lean 4 projects like "mathematics_in_lean" to work.

Kevin Buzzard (Aug 05 2023 at 18:58):

Try elan self update? You can search for this error on this Zulip, it's a common one.

George Chemmala (Aug 05 2023 at 19:13):

I've looked though Zulip and tried "elan self update" before but it hasn't worked. Moreover, elan version is "elan 2.0.1 (04475bbb5 2023-07-24)"

George Chemmala (Aug 05 2023 at 19:16):

I've seen stuff about building lean 3. I'm not exactly sure what it entails or whether I should be doing that. Should I be looking for a resource on how to do that on m1?

Alistair Tucker (Aug 05 2023 at 19:31):

It's fairly straightforward to build Lean 3 locally to get around this problem on an M1 Mac. You can follow the instructions here and finish up by running elan toolchain link.

Scott Morrison (Aug 05 2023 at 23:27):

@George C., but the more fundamental suggestion is --- unless you have a specific reason for using Lean 3 (if so, we'd be interested in what it is), you should be using Lean 4.

In my understanding, things "just work" on M1 macs with Lean 4. Moreover, Lean 3 is at end-of-life.

George Chemmala (Aug 06 2023 at 15:29):

I was just looking at an old lean 3 project that was used in a class at my university, but luckily I haven't had to deal with lean 3 too much.

How I Fixed the Error:
Find the version of lean you need from the from leanpkg.toml file in the repo

Go to https://github.com/leanprover-community/lean/releases and seach for the version you need

Download darwin zip and extact

In Terminal, cd into the extacted folder cd lean-3.##-darwin

elan toolchain link lean3.## .

open -a finder bin

Right-click lean excutable file and open. Click open when prompted with alert on the security risk of running the exceutable.

In Terminal, cd into the dir you want the repo

elan run lean3.## leanproject get [repo-author/repo]

cd [project name]

elan override set lean3.##

code .

Eric Rodriguez (Aug 23 2023 at 19:01):

btw, this thread is still linked in the how to install lean4 on MacOS thread: is this the correct way?

Eric Rodriguez (Aug 23 2023 at 19:18):

Indeed, there's an open PR that says this is not the case anymore: leanprover-community.github.io#331

Eric Rodriguez (Aug 23 2023 at 19:18):

https://github.com/leanprover-community/leanprover-community.github.io/pull/331

Eric Rodriguez (Aug 23 2023 at 19:19):

There's also #6390 that includes the script details.

Schrodinger ZHU Yifan (Aug 24 2023 at 00:47):

I think elan just works now?

Utensil Song (Sep 13 2023 at 06:36):

Is there a reason why VSCode install doesn't work for Mac M1? I also have difficulty following How to install Lean 4 on MacOS:

  1. :cross_mark: VS Code install:

error: binary package was not provided for 'darwin'

  1. :check: brew install in install_macos.sh : Almost OK, some errors but not serious
  1. :cross_mark: lake in terminal

error: binary package was not provided for 'darwin'

  1. :cross_mark: VS Code Lean 4

open a lean file, somehow lake serve started in the background but stuck there:

image.png

  1. rm -rf lake-packages & restart VS Code Lean 4 server

After inspecting the error log, I removed lake-packages and restarted Lean server.

  1. :check: VS Code Lean 4 works

  2. :check: lake in terminal works

So now I can run lake exe cache get.

What went wrong in step 4 is a special case I can ignore for now, but I wonder why step 3 (running lake in the command line) can't work, and I need VSCode Lean 4 extension to kick-start it in step 4?

(Sorry that I would have many environment issues lately, because I could open a random Lean project with Codespace(Ubuntu), CentOS 8, Mac M1, Mac non-M1, Windows, depending on where I am).

Utensil Song (Sep 13 2023 at 07:48):

I can reproduce this issue every time (after I brew uninstall elan-init and rm -rf ~/.elan then start over), namely:

  1. :cross_mark: VS Code install
  2. :check: brew install
  3. :cross_mark: lake in terminal
  4. :cross_mark: VS Code Lean 4
  5. rm -rf lake-packages& restart VS Code Lean 4 server
  6. :check: VS Code Lean 4
  7. :check: lake in terminal

I don't know how to file an issue for this, because it's an interplay between VS Code Lean 4 extension and the script/command line, and the story starts with following doc.

Scott Morrison (Sep 14 2023 at 10:54):

Sorry, I don't really understand your post.

I just installed everything on a fresh M2 mac, and everything "just worked". What do your Xs mean?

Utensil Song (Sep 14 2023 at 13:49):

Thanks! The details of every X are given in the previous message.

Utensil Song (Sep 14 2023 at 13:52):

I can get to a stable environment with the help from both the script and the extension, but not either one. It's bizarre.

Utensil Song (Sep 14 2023 at 13:53):

Also I got my M1 in 2021 and it's very alive so I don't have a M2 to test yet.

Last updated: Dec 20 2023 at 11:08 UTC