creating project on MacOS

Stream: new members

[Mike Shulman]

Up until now I have been mostly teaching my Lean 3 course without using mathlib. Today I started using mathlib more seriously for the first time, and most of my students didn't have it installed; either they hadn't created lean projects at all or their projects didn't include mathlib. I had them run leanproject new or add-mathlib or get-mathlib-cache, and it worked on the PCs but not the Macs. All the students using Macs got an error like "getting lean 3.48, no package available for darwin" (sorry, I don't remember the exact error message). Is there something different they have to do?

[Yaël Dillies]

Did they update elan? (elan self update or, if it doesn't work, uninstall and reinstall from whatever their Mac app manager is)

[Mike Shulman]

I don't know, I'll ask. Is that sometimes what that error message means?

[Mauricio Collares]

To clarify, updating elan (by trying the two things Yaël proposed) is the solution to the problem, not the cause. The error you cited was fixed in elan 1.4.2.

[Mike Shulman]

Thanks for this suggestion. Most of them got it to work by updating elan through homebrew. One or two of them installed it a different way (e.g. because they have an M1) and we're still working on it, but at least we know what the goal is...

[Mauricio Collares]

Did they install it using the instructions from https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon? If so, then they should first run arch -x86_64 zsh and then use /usr/local/bin/brew inside the resulting shell to update elan.

[Mike Shulman]

I think they did that. I'll try that with them today, thanks.