using lean3 with a M1 Prop Mac

Stream: general

[Ayhon]

I'm following a course in my university on Lean3. For the first few classes we've used the online editor, but we've been asked to install it locally in our machines and set it up to work with VSCode. However, I've been running into some problems doing so in my M1 Mac. Running elan default leanprover/lean3:v3.4.2 fails with the message

error: binary package was not provided for 'darwin_aarch64'

I've also tried to set it up in a .devcontainer, but the one I've found online (https://github.com/danielbush/lean-remote-containers) seems to install lean4 instead of lean3.

[Eric Rodriguez]

Lean3 is super unsupported, I'm afraid. It's a shame your course requires youto use it

[Eric Rodriguez]

There's some ways to install it with an M1 mac, but it's a bit of a pain, and it'll probably require you to recompile it from source (especially for such an old version).

[Yaël Dillies]

Even if it's unsupported, 3.4.2 is _ancient_. Are you sure this is the version you want to install?

[Ayhon]

It doesn't have to be 3.4.2, it's just the one I saw in the tab of the archived lean3 repository. (In realeases)

[Yaël Dillies]

Yeah that's because the Lean 3 repository was archived when work on Lean 4 started, but we kept making modifications in the "community edition". The repo is called leanprover-community/lean.

[Yaël Dillies]

If anything, you should look at leanprover-community/mathlib rather than leanprover/lean3

[Kyle Miller]

https://github.com/leanprover-community/mathlib/blob/master/leanpkg.toml shows which version of lean3 to use (leanprover-community/lean:3.51.1)