% elan toolchain list
elan toolchain list
stable (default)
leanprover-community/lean:3.42.1
leanprover-community/lean:3.49.1
leanprover/lean4:stable
leanprover/lean4:v4.4.0-rc1
leanprover/lean4:v4.5.0-rc1
4.5.0-rc1

% elan toolchain install leanprover/lean4:v4.5.0-rc1
elan toolchain install leanprover/lean4:v4.5.0-rc1

  leanprover/lean4:v4.5.0-rc1 unchanged - Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

% elan show
elan show
installed toolchains
--------------------

stable (default)
leanprover-community/lean:3.42.1
leanprover-community/lean:3.49.1
leanprover/lean4:stable
leanprover/lean4:v4.4.0-rc1
leanprover/lean4:v4.5.0-rc1
4.5.0-rc1

active toolchain
----------------

stable (default)
Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

% lean --version
lean --version
Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

% where lean
where lean
/opt/homebrew/bin/lean

% which lean
which lean
/opt/homebrew/bin/lean

(this is a symlink pointing to ../Cellar/elan-init/3.0.0/bin/lean)

% brew info lean
brew info lean
==> lean: stable 3.51.1 (bottled), HEAD
Theorem prover
https://leanprover-community.github.io/
Deprecated!
Conflicts with:
  elan-init (because `lean` and `elan-init` install the same binaries)
Not installed
From: https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/l/lean.rb
License: Apache-2.0
==> Dependencies
Build: cmake ✘
Required: coreutils ✔, gmp ✘, jemalloc ✘
==> Requirements
Required: macOS >= 10.14 (or Linux) ✔
==> Options
--HEAD
	Install HEAD version
==> Analytics
install: 22 (30 days), 115 (90 days), 501 (365 days)
install-on-request: 22 (30 days), 115 (90 days), 379 (365 days)
build-error: 0 (30 days)


% brew info elan
brew info elan
Warning: Treating elan as a formula. For the cask, use homebrew/cask/elan
==> elan-init: stable 3.0.0 (bottled), HEAD
Lean Theorem Prover installer and version manager
https://github.com/leanprover/elan
Conflicts with:
  lean (because `lean` and `elan-init` install the same binaries)
/opt/homebrew/Cellar/elan-init/3.0.0 (20 files, 4.9MB) *
  Poured from bottle using the formulae.brew.sh API on 2023-12-29 at 22:54:57
From: https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/e/elan-init.rb
License: Apache-2.0 or MIT
==> Dependencies
Build: rust ✘
Required: coreutils ✔, gmp ✘
==> Options
--HEAD
	Install HEAD version
==> Caveats
zsh completions have been installed to:
  /opt/homebrew/share/zsh/site-functions
==> Analytics
install: 164 (30 days), 545 (90 days), 1,745 (365 days)
install-on-request: 164 (30 days), 545 (90 days), 1,745 (365 days)
build-error: 0 (30 days)