math-comp.github.io/installation.org at 0c5889105ecdf34bae9cb7d994ff4350c711d758 · math-comp/math-comp.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
#+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.