#+TITLE: Mathematical Components: Installation

#+OPTIONS: toc:nil

#+OPTIONS: ^:nil

#+OPTIONS: html-postamble:nil

#+OPTIONS: num:nil

#+HTML_HEAD: <meta http-equiv="Content-Type" content="text/html; charset=utf-8">

#+HTML_HEAD: <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>

#+HTML_HEAD: <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>

#+HTML_HEAD: <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>

#+HTML_HEAD: <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>

#+HTML_HEAD: <style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>

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 [[https://opam.ocaml.org/][opam]], a

package manager for [[https://ocaml.org/][OCaml]], the programming language with which the

[[https://rocq-prover.org/][Rocq]] prover is implemented.

The relevant packages can be found in the [[https://rocq-prover.org/packages][Rocq package index]];

their name is usually prefixed with ~rocq-mathcomp-~ or ~coq-mathcomp-~.

* Install the Base Mathematical Components Libraries

** Installation using the [[https://opam.ocaml.org/][opam]] package manager

- Using opam, the installation of the base Mathematical Components

library is as simple as this:

#+BEGIN_SRC

opam repo add coq-released https://coq.inria.fr/opam/released

opam install coq-mathcomp-ssreflect

#+END_SRC

- 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 [[https://github.com/rocq-prover/platform][Coq platform]]

- The [[https://github.com/coq/platform][Coq platform]] is a distribution of [[https://rocq-prover.org/][Rocq]] 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 [[https://github.com/math-comp/math-comp/blob/master/INSTALL.md][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 instructions in [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html][Japanese, 日本語]]

+ see「パッケージからの設定」for installation using ~opam~

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

+ It is possible to install the Mathematical Components libraries on

Windows 11 using [[https://www.cygwin.com/][cygwin]] together with the binary distribution of Coq

or together with [[https://fdopen.github.io/opam-repository-mingw/installation/][opam for Windows]], or with Windows Subsystem for

Linux, as explained for example [[https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org][here]].

* Install Other Mathematical Components Libraries

There are several libraries that build on top of the base

Mathematical Components libraries, e.g.:

Extensions:

1. [[https://github.com/math-comp/finmap][Finite sets, finite maps, multisets and generic sets]]

- Available as the opam package ~coq-mathcomp-finmap~

2. [[https://github.com/math-comp/multinomials][Multinomials for the Mathematical Components library]]

- Available as the opam package ~coq-mathcomp-multinomials~

3. [[https://github.com/math-comp/real-closed][Theorems for Real Closed Fields]]

- Available as the opam package ~coq-mathcomp-real-closed~

4. A layer for classical reasoning (developed along [[https://github.com/math-comp/analysis][MathComp Analysis]])

- Available as the opam package ~coq-mathcomp-classical~

4. [[https://github.com/math-comp/analysis][MathComp Analysis]]

- Available as the opam package ~coq-mathcomp-analysis~

Applications:

1. [[https://github.com/math-comp/fourcolor][The Four Color theorem]]

- Available as the opam package ~coq-fourcolor~

2. [[https://github.com/math-comp/odd-order][The Odd Order theorem]]

- Available as the opam package ~coq-mathcomp-odd-order~

3. [[https://github.com/math-comp/Abel][Abel-Ruffini theorem]]

- Available as the opam package ~coq-mathcomp-abel~

4. [[https://github.com/coq-community/apery][A formal proof of the irrationality of zeta(3), the Apéry constant]]

- Available as the opam package ~coq-mathcomp-apery~

More libraries:

- See the Mathematical Components' [[https://github.com/math-comp][github]].

- [[https://rocq-community.org/][rocq-community]] also features a number of libraries using Mathematical Components.