Mathematical Components: Installation

Install the Base Mathematical Components Libraries

Installation using the opam package manager

  • The installation of Mathematical Components can be done using opam, a package manager for OCaml, the programming language with which Coq is implemented.
  • Using opam, the installation of the base Mathematical Components library is as simple as this:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect
  • Other base mathematical components libraries can then be installed similarly using opam install. The available packages can be found in the Coq package index:
    • coq-mathcomp-algebra,
    • coq-mathcomp-field,
    • coq-mathcomp-solvable,
    • coq-mathcomp-fingroup,
    • coq-mathcomp-character.
  • You can find more detailed installation instructions in INSTALL.md (from the official distribution), this includes:
    • various ways of installing using opam
    • installation from the source files (using make)
    • installation using nix

Installation using the Coq platform

  • The Coq platform is a distribution of Coq together with a selection of libraries including most Mathematical Components libraries. It supports Linux, macOS, and Windows.

Installation Instructions in Other Languages

  • Installation instructions in Japanese, 日本語
    • see「パッケージからの設定」for installation using opam

Advanced: Installation Instructions for Windows 10 & 11 using cygwin-opam or WSL

  • It is possible to install the Mathematical Components libraries on Windows 10 & 11 using cygwin together with the binary distribution of Coq or together with opam for Windows, or with Windows Subsystem for Linux, as explained for example here

Other Mathematical Components Libraries

There are already several libraries that build on top of the base Mathematical Components libraries:

  1. The Four Color theorem
    • Available as the opam package coq-fourcolor
  2. The Odd Order theorem
    • Available as the opam package coq-mathcomp-odd-order
  3. MathComp Analysis
    • Available as the opam package coq-mathcomp-analysis
  4. Abel-Ruffini theorem
    • Available as the opam package coq-mathcomp-abel
  5. Theorems for Real Closed Fields
    • Available as the opam package coq-mathcomp-real-closed
  6. Finite sets, finite maps, multisets and generic sets
    • Available as the opam package coq-mathcomp-finmap
  7. Multinomials for the Mathematical Components library
    • Available as the opam package coq-mathcomp-multinomials
  8. A formal proof of the irrationality of zeta(3), the Apéry constant
    • Available as the opam package coq-mathcomp-apery
  9. See the Mathematical Components' github for more libraries. coq-community also features a number of libraries using Mathematical Components.