-
Notifications
You must be signed in to change notification settings - Fork 22
/
meta.yml
121 lines (96 loc) · 3.23 KB
/
meta.yml
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
fullname: The Four Color Theorem
shortname: fourcolor
organization: coq-community
community: true
action: true
synopsis: >-
Mechanization of the Four Color Theorem in Coq
description: |-
This library contains a formal proof of the Four Color Theorem in Coq,
along with the theories needed to support stating and then proving the Theorem.
This includes an axiomatization of the setoid of classical real numbers,
basic plane topology definitions, and a theory of combinatorial hypermaps.
publications:
- pub_url: https://www.ams.org/notices/200811/tx081101382p.pdf
pub_title: Formal Proof—The Four-Color Theorem
- pub_url: https://inria.hal.science/hal-04034866/document
pub_title: A computer-checked proof of the Four Color Theorem
authors:
- name: Georges Gonthier
initial: true
maintainers:
- name: Yves Bertot
nickname: ybertot
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
supported_coq_versions:
text: 8.16 or later
opam: '{>= "8.16"}'
tested_coq_opam_versions:
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
# test master every Sunday at 05:00 UTC
# (mathcomp/mathcomp-dev is rebuilt every day at 04:00 Paris time)
ci_cron_schedule: '0 5 * * 0'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.1.0"}'
description: |-
[MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-hierarchy-builder
version: '{>= "1.5.0"}'
description: |-
[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
namespace: fourcolor
keywords:
- name: Four color theorem
- name: small scale reflection
- name: Mathematical Components
categories:
- name: Mathematics/Combinatorics and Graph Theory
build: |-
## Building and installation instructions
The easiest way to install the latest released version of The Four Color Theorem
is via [opam](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor
```
If you are only interested in the formalization of real numbers, you can install
it separately:
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor-reals
```
To instead build and install the whole project manually from the repository, do:
``` shell
git clone https://github.com/coq-community/fourcolor.git
cd fourcolor
make # or make -j <number-of-cores-on-your-machine>
make install
```
documentation: |-
## Documentation
The [Four Color Theorem](https://en.wikipedia.org/wiki/Four_color_theorem) (Appel & Haken, 1976) is a landmark result of graph theory.
The formal proof is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library.