Lean 3 & the new elan on ARM Mac

Of course, Lean 3 is now deprecated. But you may still want to access old Lean 3 projects.

The latest version of elan (3.1.1) can’t automatically install Lean 3 toolchains (at least not on a Mac with an ARM CPU). For example, if you have cloned a Lean 3 repo and try to run leanpkg configure, you’ll get an error message:

error: binary package was not provided for 'darwin_aarch64'

A solution is provided by George Chemmala on the Lean Zulip chat. Here’s the idea:

• Locate the desired lean release, then download and extract the darwin zip. In this example, I’ll suppose you are using Lean version 3.42.1.
• Suppose you have downloaded and extracted lean-3.42.1-darwin to your Downloads directory. Move it to somewhere else. For example, you might move it to ~/Documents/mytoolchains/lean-3.42.1-darwin.
• Open a terminal at this new directory and run:
  elan toolchain link lean-3.42.1 .
  This creates installs the toolchain (via a symlink to the current directory) and calls the toolchain lean-3.42.1.
• Unfortunately, your job isn’t over! In any project that depends on Lean 3.42.1, you need to let elan know to use the downloaded toolchain (else it will try and fail to download the darwin binaries). To do this, change directory to the root of your project and type
  elan override set lean-3.42.1