-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathindex.html
341 lines (324 loc) · 15.2 KB
/
index.html
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2024-11-28 Thu 12:40 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Mathematical Components</title>
<meta name="author" content="Laurent Thery" />
<meta name="generator" content="Org Mode" />
<style>
#content { max-width: 60em; margin: auto; }
.title { text-align: center;
margin-bottom: .2em; }
.subtitle { text-align: center;
font-size: medium;
font-weight: bold;
margin-top:0; }
.todo { font-family: monospace; color: red; }
.done { font-family: monospace; color: green; }
.priority { font-family: monospace; color: orange; }
.tag { background-color: #eee; font-family: monospace;
padding: 2px; font-size: 80%; font-weight: normal; }
.timestamp { color: #bebebe; }
.timestamp-kwd { color: #5f9ea0; }
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
.underline { text-decoration: underline; }
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
p.verse { margin-left: 3%; }
pre {
border: 1px solid #e6e6e6;
border-radius: 3px;
background-color: #f2f2f2;
padding: 8pt;
font-family: monospace;
overflow: auto;
margin: 1.2em;
}
pre.src {
position: relative;
overflow: auto;
}
pre.src:before {
display: none;
position: absolute;
top: -8px;
right: 12px;
padding: 3px;
color: #555;
background-color: #f2f2f299;
}
pre.src:hover:before { display: inline; margin-top: 14px;}
/* Languages per Org manual */
pre.src-asymptote:before { content: 'Asymptote'; }
pre.src-awk:before { content: 'Awk'; }
pre.src-authinfo::before { content: 'Authinfo'; }
pre.src-C:before { content: 'C'; }
/* pre.src-C++ doesn't work in CSS */
pre.src-clojure:before { content: 'Clojure'; }
pre.src-css:before { content: 'CSS'; }
pre.src-D:before { content: 'D'; }
pre.src-ditaa:before { content: 'ditaa'; }
pre.src-dot:before { content: 'Graphviz'; }
pre.src-calc:before { content: 'Emacs Calc'; }
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
pre.src-fortran:before { content: 'Fortran'; }
pre.src-gnuplot:before { content: 'gnuplot'; }
pre.src-haskell:before { content: 'Haskell'; }
pre.src-hledger:before { content: 'hledger'; }
pre.src-java:before { content: 'Java'; }
pre.src-js:before { content: 'Javascript'; }
pre.src-latex:before { content: 'LaTeX'; }
pre.src-ledger:before { content: 'Ledger'; }
pre.src-lisp:before { content: 'Lisp'; }
pre.src-lilypond:before { content: 'Lilypond'; }
pre.src-lua:before { content: 'Lua'; }
pre.src-matlab:before { content: 'MATLAB'; }
pre.src-mscgen:before { content: 'Mscgen'; }
pre.src-ocaml:before { content: 'Objective Caml'; }
pre.src-octave:before { content: 'Octave'; }
pre.src-org:before { content: 'Org mode'; }
pre.src-oz:before { content: 'OZ'; }
pre.src-plantuml:before { content: 'Plantuml'; }
pre.src-processing:before { content: 'Processing.js'; }
pre.src-python:before { content: 'Python'; }
pre.src-R:before { content: 'R'; }
pre.src-ruby:before { content: 'Ruby'; }
pre.src-sass:before { content: 'Sass'; }
pre.src-scheme:before { content: 'Scheme'; }
pre.src-screen:before { content: 'Gnu Screen'; }
pre.src-sed:before { content: 'Sed'; }
pre.src-sh:before { content: 'shell'; }
pre.src-sql:before { content: 'SQL'; }
pre.src-sqlite:before { content: 'SQLite'; }
/* additional languages in org.el's org-babel-load-languages alist */
pre.src-forth:before { content: 'Forth'; }
pre.src-io:before { content: 'IO'; }
pre.src-J:before { content: 'J'; }
pre.src-makefile:before { content: 'Makefile'; }
pre.src-maxima:before { content: 'Maxima'; }
pre.src-perl:before { content: 'Perl'; }
pre.src-picolisp:before { content: 'Pico Lisp'; }
pre.src-scala:before { content: 'Scala'; }
pre.src-shell:before { content: 'Shell Script'; }
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
/* additional language identifiers per "defun org-babel-execute"
in ob-*.el */
pre.src-cpp:before { content: 'C++'; }
pre.src-abc:before { content: 'ABC'; }
pre.src-coq:before { content: 'Coq'; }
pre.src-groovy:before { content: 'Groovy'; }
/* additional language identifiers from org-babel-shell-names in
ob-shell.el: ob-shell is the only babel language using a lambda to put
the execution function name together. */
pre.src-bash:before { content: 'bash'; }
pre.src-csh:before { content: 'csh'; }
pre.src-ash:before { content: 'ash'; }
pre.src-dash:before { content: 'dash'; }
pre.src-ksh:before { content: 'ksh'; }
pre.src-mksh:before { content: 'mksh'; }
pre.src-posh:before { content: 'posh'; }
/* Additional Emacs modes also supported by the LaTeX listings package */
pre.src-ada:before { content: 'Ada'; }
pre.src-asm:before { content: 'Assembler'; }
pre.src-caml:before { content: 'Caml'; }
pre.src-delphi:before { content: 'Delphi'; }
pre.src-html:before { content: 'HTML'; }
pre.src-idl:before { content: 'IDL'; }
pre.src-mercury:before { content: 'Mercury'; }
pre.src-metapost:before { content: 'MetaPost'; }
pre.src-modula-2:before { content: 'Modula-2'; }
pre.src-pascal:before { content: 'Pascal'; }
pre.src-ps:before { content: 'PostScript'; }
pre.src-prolog:before { content: 'Prolog'; }
pre.src-simula:before { content: 'Simula'; }
pre.src-tcl:before { content: 'tcl'; }
pre.src-tex:before { content: 'TeX'; }
pre.src-plain-tex:before { content: 'Plain TeX'; }
pre.src-verilog:before { content: 'Verilog'; }
pre.src-vhdl:before { content: 'VHDL'; }
pre.src-xml:before { content: 'XML'; }
pre.src-nxml:before { content: 'XML'; }
/* add a generic configuration mode; LaTeX export needs an additional
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
pre.src-conf:before { content: 'Configuration File'; }
table { border-collapse:collapse; }
caption.t-above { caption-side: top; }
caption.t-bottom { caption-side: bottom; }
td, th { vertical-align:top; }
th.org-right { text-align: center; }
th.org-left { text-align: center; }
th.org-center { text-align: center; }
td.org-right { text-align: right; }
td.org-left { text-align: left; }
td.org-center { text-align: center; }
dt { font-weight: bold; }
.footpara { display: inline; }
.footdef { margin-bottom: 1em; }
.figure { padding: 1em; }
.figure p { text-align: center; }
.equation-container {
display: table;
text-align: center;
width: 100%;
}
.equation {
vertical-align: middle;
}
.equation-label {
display: table-cell;
text-align: right;
vertical-align: middle;
}
.inlinetask {
padding: 10px;
border: 2px solid gray;
margin: 10px;
background: #ffffcc;
}
#org-div-home-and-up
{ text-align: right; font-size: 70%; white-space: nowrap; }
textarea { overflow-x: auto; }
.linenr { font-size: smaller }
.code-highlighted { background-color: #ffff00; }
.org-info-js_info-navigation { border-style: none; }
#org-info-js_console-label
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
.org-info-js_search-highlight
{ background-color: #ffff00; color: #000000; font-weight: bold; }
.org-svg { }
</style>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
<style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>
</head>
<body>
<div id="content" class="content">
<h1 class="title">Mathematical Components</h1>
<p>
<div style="text-align:right"><img src="github-mark.png" height="25" style="border:0px">
<a href="https://github.com/math-comp/">View the Project on GitHub</a>
<img src="github-mark.png" height="25" style="border:0px"></div>
</p>
<div id="outline-container-org75bbace" class="outline-2">
<h2 id="org75bbace">About</h2>
<div class="outline-text-2" id="text-org75bbace">
<p>
Welcome to Mathematical Components' web-page!
</p>
<p>
Mathematical Components are libraries of formalized mathematics
developed using the <a href="http://coq.inria.fr">Coq</a> proof assistant. This project finds its roots
in the formal proof of the Four Color Theorem. It has been used for
large scale formalization projects, including a formal proof of the
Odd Order
(Feit-Thompson) Theorem.
</p>
<p>
The libraries are written using the Ssreflect proof language, now part of
the standard distribution of the Coq proof assistant.
</p>
<p>
This is an open source project, licensed under the CeCILL-B free
software license agreement.
</p>
</div>
</div>
<div id="outline-container-org78db00d" class="outline-2">
<h2 id="org78db00d">Get the library</h2>
<div class="outline-text-2" id="text-org78db00d">
<ul class="org-ul">
<li>The last stable releases of the Mathematical Components library
can be <a href="https://github.com/math-comp/math-comp/releases">downloaded from github</a>.</li>
<li><a href="installation.html">Installation instructions</a>.</li>
<li>Older versions of the Mathematical Components library are also available
(<a href="https://github.com/math-comp/math-comp/releases/tag/archive">historical archives</a> (2008-2014), <a href="https://github.com/math-comp/mathcomp-history-before-github">pre-github archive</a>)</li>
</ul>
</div>
</div>
<div id="outline-container-org95a592b" class="outline-2">
<h2 id="org95a592b">Documentation</h2>
<div class="outline-text-2" id="text-org95a592b">
<div style="float: right; width: 240px; margin: 5px 10px">
<a href="https://math-comp.github.io/mcb/"><img alt="Mathematical Components book" src="https://math-comp.github.io/mcb/cover-front-web.png" style="width: 240px" border="1px solid black"></a>
</div>
<ul class="org-ul">
<li>The source file of each library features a documentation header
which describes the concepts and notations introduced in that library.</li>
<li>The library graph can be explored interactively and the coqdoc
presentation of the source files can be browsed online:
<ul class="org-ul">
<li>latest versions:
<ul class="org-ul">
<li>Version 2.3.0 (2024-11-28): <a href="htmldoc_2_3_0/libgraph.html">library graph</a>, <a href="htmldoc_2_3_0/index.html">coqdoc presentation</a></li>
<li>Version 2.2.0 (2024-01-17): <a href="htmldoc_2_2_0/libgraph.html">library graph</a>, <a href="htmldoc_2_2_0/index.html">coqdoc presentation</a></li>
<li>Version 1.19.0 (2024-01-15): <a href="htmldoc_1_19_0/libgraph.html">library graph</a>, <a href="htmldoc_1_19_0/index.html">coqdoc presentation</a></li>
</ul></li>
<li>older versions:
<ul class="org-ul">
<li>Version 2.1.0 (2023-10-24): <a href="htmldoc_2_1_0/libgraph.html">library graph</a>, <a href="htmldoc_2_1_0/index.html">coqdoc presentation</a></li>
<li>Version 2.0.0 (2023-05-10): <a href="htmldoc_2_0_0/libgraph.html">library graph</a>, <a href="htmldoc_2_0_0/index.html">coqdoc presentation</a></li>
<li>Version 1.18.0 (2023-11-01): <a href="htmldoc_1_18_0/libgraph.html">library graph</a>, <a href="htmldoc_1_18_0/index.html">coqdoc presentation</a></li>
<li>Version 1.17.0 (2023-05-09): <a href="htmldoc_1_17_0/libgraph.html">library graph</a>, <a href="htmldoc_1_17_0/index.html">coqdoc presentation</a></li>
<li>Version 1.16.0 (2023-02-01): <a href="htmldoc_1_16_0/libgraph.html">library graph</a>, <a href="htmldoc_1_16_0/index.html">coqdoc presentation</a></li>
<li>Version 2.0+alpha1 (2022-12-05): <a href="htmldoc_2_0_alpha1/libgraph.html">library graph</a>, <a href="htmldoc_2_0_alpha1/index.html">coqdoc presentation</a></li>
<li>Version 1.15.0 (2022-06-30): <a href="htmldoc_1_15_0/libgraph.html">library graph</a>, <a href="htmldoc_1_15_0/index.html">coqdoc presentation</a></li>
<li>Version 1.14.0 (2022-01-19): <a href="htmldoc_1_14_0/libgraph.html">library graph</a>, <a href="htmldoc_1_14_0/index.html">coqdoc presentation</a></li>
<li>Version 1.13.0 (2021-10-28): <a href="htmldoc_1_13_0/libgraph.html">library graph</a>, <a href="htmldoc_1_13_0/index.html">coqdoc presentation</a></li>
<li>Version 1.12.0 (2020-11-26): <a href="htmldoc_1_12_0/libgraph.html">library graph</a>, <a href="htmldoc_1_12_0/index.html">coqdoc presentation</a></li>
<li>Version 1.11.0 (2020-06-09): <a href="htmldoc_1_11_0/libgraph.html">library graph</a>, <a href="htmldoc_1_11_0/index.html">coqdoc presentation</a></li>
<li>Version 1.10.0 (2019-11-29): <a href="htmldoc_1_10_0/libgraph.html">library graph</a>, <a href="htmldoc_1_10_0/index.html">coqdoc presentation</a></li>
</ul></li>
</ul></li>
<li>The Ssreflect language comes with a dedicated reference manual,
as a <a href="https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html">chapter</a> of Coq's reference manual.</li>
<li>A <a href="https://math-comp.github.io/mcb/">book</a> that introduces the techniques for writing
algorithms and proofs and describes the design ideas of the
library.</li>
</ul>
</div>
<div id="outline-container-org28a97fe" class="outline-3">
<h3 id="org28a97fe">More material</h3>
<div class="outline-text-3" id="text-org28a97fe">
<ul class="org-ul">
<li><a href="documentation.html">Books, lectures, videos, etc.</a></li>
<li><a href="papers.html">Research papers</a> related to Mathematical Components. Your paper or
thesis is not in the list? Send <a href="mailto:[email protected]?subject=MathComp%20related%20paper">us</a> a message to correct this.</li>
</ul>
</div>
</div>
</div>
<div id="outline-container-org3c200e4" class="outline-2">
<h2 id="org3c200e4">Help and contact</h2>
<div class="outline-text-2" id="text-org3c200e4">
<ul class="org-ul">
<li>Chat with us on <a href="https://coq.zulipchat.com/">Coq's Zulip</a>!</li>
<li>Discuss with us on Coq's <a href="https://coq.discourse.group/">Discourse</a> forum!</li>
<li><a href="mailto:[email protected]?subject=SUBSCRIBE%20ssreflect">Subscribe</a> to the Ssreflect mailing list.
<ul class="org-ul">
<li>Browse the <a href="https://sympa.inria.fr/sympa/arc/ssreflect">archives</a> or consult the general <a href="https://sympa.inria.fr/sympa/info/ssreflect">information page</a> of the mailing list.</li>
</ul></li>
</ul>
</div>
</div>
<div id="outline-container-org2ac74b6" class="outline-2">
<h2 id="org2ac74b6">Authors and contributors</h2>
<div class="outline-text-2" id="text-org2ac74b6">
<p>
The Mathematical Components library and the Ssreflect proof language
were initially developed by the Mathematical Components team at the
<a href="https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/">Inria-Microsoft Research Joint Center</a>. Today, the list of members of
the Mathematical Components organization is visible <a href="https://github.com/orgs/math-comp/people">here</a>.
</p>
</div>
</div>
</div>
</body>
</html>