|
24 | 24 | <a id="about" class="anchor" href="#about" aria-hidden="true"><span class="octicon octicon-link"></span></a>About</h3>
|
25 | 25 |
|
26 | 26 | <p>
|
27 |
| -Mathematical Components is the name of a library of formalized mathematics for |
28 |
| -the Coq system. It covers a variety of topics, from the theory of basic data |
29 |
| -structures (e.g., numbers, lists, finite sets) to advanced results in various |
30 |
| -flavors of algebra. This library constitutes the infrastructure for the machine |
| 27 | +Mathematical Components is the name of a library of formalized |
| 28 | +mathematics for the Coq proof assistants. It covers a variety of |
| 29 | +topics, from the theory of basic data structures (e.g., numbers, |
| 30 | +lists, finite sets) to more advanced results in various flavors of |
| 31 | +algebra. This library constitutes the infrastructure for the machine |
31 | 32 | checked proofs of the Four Color Theorem and of the Odd Order Theorem.
|
32 | 33 | </p>
|
33 | 34 | <p>
|
34 |
| -The reason of existence of this book is to break down the barriers to entry. |
35 |
| -While there are several books around covering the usage of the Coq system and |
36 |
| -the theory it is based on, the Mathematical Components library is built in an |
37 |
| -unconventional way. As a consequence this book provides a non standard |
38 |
| -presentation of Coq, putting upfront the formalization choices and the proof |
39 |
| -style that are the pillars of the library. |
| 35 | +This book aims at providing an introducing to the design patterns used |
| 36 | +throughout this library, so as to ease its use for other projects. |
| 37 | +While there are several books around covering the usage of the Coq |
| 38 | +system and the theory it is based on, the Mathematical Components |
| 39 | +library uses a few design patterns that differ from the methodology |
| 40 | +propose in other sources. As a consequence, this book provides a |
| 41 | +slightly non-standard presentation of Coq, putting upfront the |
| 42 | +formalization choices and the proof style that are the pillars of the |
| 43 | +library. |
40 | 44 | </p>
|
41 | 45 | <p>
|
42 |
| -This books targets two classes of public. On one hand newcomers, even the more |
43 |
| -mathematical inclined ones, find a soft introduction to the programming |
44 |
| -language of Coq, <em>Gallina</em>, and the <em>Ssreflect</em> proof language. |
45 |
| -On the other hand accustomed Coq users find a substantial account of the |
46 |
| -formalization style that made the Mathematical Components library possible. |
| 46 | +This books targets two natures of audience. On one hand newcomers, in |
| 47 | +particular beginners with background in mathematics rather than |
| 48 | +computer science, should find a soft introduction to the programming |
| 49 | +language of Coq, <em>Gallina</em>, and to the <em>Ssreflect</em> proof |
| 50 | +language. On the other hand, accustomed Coq users will find a |
| 51 | +substantial account of the formalization style that made the |
| 52 | +Mathematical Components library possible. |
47 | 53 | </p>
|
48 | 54 |
|
49 | 55 | <h3>
|
50 | 56 | <a id="releases" class="anchor" href="#releases" aria-hidden="true"><span class="octicon octicon-link"></span></a>Getting the book</h3>
|
51 | 57 |
|
52 | 58 | <p>
|
53 |
| -The book in <a href="book.pdf">PDF format</a>. |
54 |
| -<!--date-->(last update Sat Aug 11 18:12:20 CEST 2018) |
| 59 | +Download the book in <a href="https://zenodo.org/record/3999478">PDF format</a>. |
| 60 | +<a href="https://doi.org/10.5281/zenodo.3999478">Cite</a> it. |
55 | 61 | </p>
|
56 | 62 |
|
57 |
| -<p> |
58 |
| -The book printed on demand (TBD) |
59 |
| -</p> |
60 | 63 |
|
61 |
| -<p> |
62 |
| -Coq snippets that can be played in the browser thanks |
63 |
| -to <a href="https://github.com/ejgallego/jscoq">jscoq</a>:<br/> |
64 |
| -<a href="ch0.html">ch0</a>, |
65 |
| -<a href="ch1.html">ch1</a>, |
66 |
| -<a href="ch2.html">ch2</a>, |
67 |
| -<a href="ch3.html">ch3</a>, |
68 |
| -<a href="ch4.html">ch4</a>, |
69 |
| -<a href="ch6.html">ch6</a>, |
70 |
| -<a href="ch7.html">ch7</a>. |
71 |
| -</p> |
| 64 | +<!-- <p> --> |
| 65 | +<!-- Coq snippets that can be played in the browser thanks --> |
| 66 | +<!-- to <a href="https://github.com/ejgallego/jscoq">jscoq</a>:<br/> --> |
| 67 | +<!-- <a href="ch0.html">ch0</a>, --> |
| 68 | +<!-- <a href="ch1.html">ch1</a>, --> |
| 69 | +<!-- <a href="ch2.html">ch2</a>, --> |
| 70 | +<!-- <a href="ch3.html">ch3</a>, --> |
| 71 | +<!-- <a href="ch4.html">ch4</a>, --> |
| 72 | +<!-- <a href="ch6.html">ch6</a>, --> |
| 73 | +<!-- <a href="ch7.html">ch7</a>. --> |
| 74 | +<!-- </p> --> |
72 | 75 |
|
73 | 76 | <p>
|
74 | 77 | Feedback on the book is very welcome. Issues can be reported on the
|
|
88 | 91 | <a id="contact" class="anchor" href="#contact" aria-hidden="true"><span class="octicon octicon-link"></span></a>Join the community of users</h3>
|
89 | 92 |
|
90 | 93 | <p>
|
91 |
| -Interested? |
92 |
| -<a href="mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect">Subscribe to the ssreflect mailing list</a> |
93 |
| -and let us know what you are using our libraries for, ask questions, etc. |
94 |
| -You can also browse the <a href="https://sympa.inria.fr/sympa/info/ssreflect">archives of the list</a>. |
| 94 | +Interested? Chat with us on |
| 95 | +<a href="https://coq.zulipchat.com/">Zulip</a>. |
95 | 96 | </p>
|
96 | 97 |
|
97 | 98 | <h3>
|
|
0 commit comments