mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
e3517f1c86
This PR brings the Mac OSX build instructions up to date slightly. (They currently refer to facts "...as of November 2014...") - Remove specific OS version number from the title as it is out of date with respect to filename. - Nonetheless don't change filename for the sake of not breaking incoming links. - Update C++ language version to C++14, which I believe is what is currently required, based on other platform documentation. - Bump versions of C++ compilers that seem to be current. I expect the exact values of these version numbers aren't crucial but maybe good for the reader calibrating a vague sense of whether their compiler is in the right ballpark. - Add `lld` to the homebrew clang instructions, because homebrew changed the way they package llvm tools, spinning the linker off into its own package.
1.1 KiB
1.1 KiB
Install Packages on OS X
We assume that you are using homebrew as a package manager.
Compilers
You need a C++14-compatible compiler to build Lean. As of July 2025, you have three options:
- clang++ shipped with OSX (at time of writing v17.0.0)
- clang++ via homebrew (at time of writing, v20.1.8)
- gcc via homebrew (at time of writing, v15.1.0)
We recommend to use Apple's clang++ because it is pre-shipped with OS X and requires no further installation.
To install gcc via homebrew, please execute:
brew install gcc
To install clang via homebrew, please execute:
brew install llvm lld
To use compilers other than the default one (Apple's clang++), you
need to use -DCMAKE_CXX_COMPILER option to specify the compiler
that you want to use when you run cmake. For example, do the
following to use g++.
cmake -DCMAKE_CXX_COMPILER=g++ ...
Required Packages: CMake, GMP, libuv, pkgconf
brew install cmake
brew install gmp
brew install libuv
brew install pkgconf
Recommended Packages: CCache
brew install ccache