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
- various ways of installing using
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
- see「パッケージからの設定」for installation using
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:
- 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
- MathComp Analysis
- Available as the opam package
coq-mathcomp-analysis
- Available as the opam package
- Abel-Ruffini theorem
- Available as the opam package
coq-mathcomp-abel
- Available as the opam package
- Theorems for Real Closed Fields
- Available as the opam package
coq-mathcomp-real-closed
- Available as the opam package
- 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
- 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
- See the Mathematical Components' github for more libraries. coq-community also features a number of libraries using Mathematical Components.