Mathematical Components: Installation
The Mathematical Components libraries are provided as separate packages:
- The base libraries are the libraries that support the formalization of the Four Color Theorem and of the Odd Order Theorem.
- Other libraries contain extensions and applications.
The installation of Mathematical Components is best done using opam, a package manager for OCaml, the programming language with which Coq is implemented.
The relevant packages can be found in the Coq package index;
their name is usually prefixed with coq-mathcomp-.
Install the Base Mathematical Components Libraries
Installation using the opam package manager
- 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:coq-mathcomp-algebra,coq-mathcomp-field,coq-mathcomp-solvable,coq-mathcomp-fingroup,coq-mathcomp-character.
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.
Other installation instructions and details
- 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
- various ways of installing using
- Installation instructions in Japanese, 日本語
- see「パッケージからの設定」for installation using
opam
- see「パッケージからの設定」for installation using
- Advanced: Installation Instructions for Windows 11 using cygwin-opam or WSL
- It is possible to install the Mathematical Components libraries on Windows 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.
Install Other Mathematical Components Libraries
There are several libraries that build on top of the base Mathematical Components libraries, e.g.:
Extensions:
- Finite sets, finite maps, multisets and generic sets
- Available as the opam package
coq-mathcomp-finmap
- Available as the opam package
- Multinomials for the Mathematical Components library
- Available as the opam package
coq-mathcomp-multinomials
- Available as the opam package
- Theorems for Real Closed Fields
- Available as the opam package
coq-mathcomp-real-closed
- Available as the opam package
- A layer for classical reasoning (developed along MathComp Analysis)
- Available as the opam package
coq-mathcomp-classical
- Available as the opam package
- MathComp Analysis
- Available as the opam package
coq-mathcomp-analysis
- Available as the opam package
Applications:
- The Four Color theorem
- Available as the opam package
coq-fourcolor
- Available as the opam package
- The Odd Order theorem
- Available as the opam package
coq-mathcomp-odd-order
- Available as the opam package
- Abel-Ruffini theorem
- Available as the opam package
coq-mathcomp-abel
- Available as the opam package
- A formal proof of the irrationality of zeta(3), the Apéry constant
- Available as the opam package
coq-mathcomp-apery
- Available as the opam package
More libraries:
- See the Mathematical Components' github.
- coq-community also features a number of libraries using Mathematical Components.