Mathematical Components: Installation

Install the Base Mathematical Components Libraries

  • The installation of Mathematical Components is best 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 be installed similarly using opam install. The available packages can be found in the Coq package index, e.g.:
    • coq-mathcomp-algebra,
    • coq-mathcomp-field,
    • etc.
  • 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)
    • more to come (using nix)

Installation Instructions in Other Languages

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

Installation Instructions for Windows 10

  • It is possible to install the Mathematical Components libraries on Windows 10 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
  4. See the Mathematical Components' github for more libraries