Lean v3.48.0 on MacOS

Stream: new members

[Michał Mrugała]

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]

Can you reinstall elan?

[Kevin Buzzard]

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]

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]

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