Zulip Chat Archive

Stream: new members

Topic: Lean v3.48.0 on MacOS

Michał Mrugała (Sep 26 2022 at 13:21):

Hello everyone,

I'm running into an issue with configuring the newest lean version on MacOS. Whenever I try to run leanpkg configure I get an error saying that the binary package was not provided for 'darwin'. Would anyone know how I could try to resolve this issue?

Eric Wieser (Sep 26 2022 at 14:42):

Can you reinstall elan?

Kevin Buzzard (Sep 26 2022 at 18:50):

Does the method for reinstalling elan depend on either or both of (1) whether you're on M1 and (2) how you installed it in the past? @Michał Mrugała do you have enough clues to fix this? You're attending my workshop this week, right? I was rather hoping that everyone would be up and running by Monday evening.

Mauricio Collares (Sep 26 2022 at 19:32):

The procedure should be: Run /usr/local/bin/brew install elan-init. If that works, you're good to go. If it fails with a "No such file" error, run brew install elan-init.

Michał Mrugała (Sep 27 2022 at 08:55):

Thank you all, reinstalling elan after unshallowing homebrew fixed the issue.

Last updated: Dec 20 2023 at 11:08 UTC