Installation of Coq on Mac
The recommended installation method is through the Coq platform. Other installation methods are also documented below.
The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install opam, Coq, external Coq libraries and Coq plugins on macOS, Windows and many Linux distributions in a reliable way with consistent results.
Binary installers for the Coq platform on macOS are not yet available. In the meantime, binary installers for just Coq + CoqIDE on macOS can be found at https://github.com/coq/coq/releases/latest.
Experienced users can rely on the Coq platform interactive scripts to install the Coq platform from sources using opam. This will create an opam switch with Coq and a standard set of packages, which can then be modified, e.g., by installing additional packages.
See the macOS specific instructions for the Coq platform scripts here: https://github.com/coq/platform/blob/2021.02/README_macOS.md
Once the Coq platform is set up, you can install additional Coq packages by running opam install coq-packagename.
You will need a user interface to run Coq. The Coq platform bundles CoqIDE, which is a Coq-specific editor. Alternatively, you can install editor-support packages for VsCode, Emacs or Vim. See https://coq.inria.fr/user-interfaces.html for details.
Complete instructions are available at https://coq.inria.fr/opam-using.html. They can be useful if you need to manage several versions of Coq and use specific versions of the OCaml compiler. Otherwise, we advise installing Coq through the Coq platform interactive scripts (see above).
You can install Coq with Homebrew by simply running
brew install coq
or using MacPorts by running
sudo port install coq
or using the Nix package manager running
nix-env -iA nixpkgs.coq
You can check that your installation was successful by running coqc -v.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.