From 2210615d1e227def9a0d22d99b2922d7c7fddb9d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 13 Nov 2025 11:10:03 +0900 Subject: [PATCH] move older versions to dedicated page - also update a few links to Rocq --- history.html | 234 ++++++++++++++++++++++++++++++++++++++++++++++ history.org | 32 +++++++ index.html | 189 ++++++++++++------------------------- index.org | 69 ++++++-------- installation.html | 127 ++++++++----------------- installation.org | 14 +-- 6 files changed, 397 insertions(+), 268 deletions(-) create mode 100644 history.html create mode 100644 history.org diff --git a/history.html b/history.html new file mode 100644 index 00000000..8642121f --- /dev/null +++ b/history.html @@ -0,0 +1,234 @@ + + + + + + + +Past releases of the Mathematical Components library + + + + + + + + + + + +
+

Past releases of the Mathematical Components library

+ +
+ + diff --git a/history.org b/history.org new file mode 100644 index 00000000..7a761865 --- /dev/null +++ b/history.org @@ -0,0 +1,32 @@ +#+TITLE: Past releases of the Mathematical Components library +#+OPTIONS: toc:nil +#+OPTIONS: ^:nil +#+OPTIONS: html-postamble:nil +#+OPTIONS: num:nil +#+HTML_HEAD: +#+HTML_HEAD: +#+HTML_HEAD: +#+HTML_HEAD: +#+HTML_HEAD: +#+HTML_HEAD: + +- Graph of the files of the Mathematical Components library and HTML + rendering to be explored interactively online: + + Version 2.1.0 (2023-10-24): [[file:htmldoc_2_1_0/libgraph.html][library graph]], [[file:htmldoc_2_1_0/index.html][coqdoc presentation]] + + Version 2.0.0 (2023-05-10): [[file:htmldoc_2_0_0/libgraph.html][library graph]], [[file:htmldoc_2_0_0/index.html][coqdoc presentation]] + + Version 1.19.0 (2024-01-15): [[file:htmldoc_1_19_0/libgraph.html][library graph]], [[file:htmldoc_1_19_0/index.html][coqdoc presentation]] + + Version 1.18.0 (2023-11-01): [[file:htmldoc_1_18_0/libgraph.html][library graph]], [[file:htmldoc_1_18_0/index.html][coqdoc presentation]] + + Version 1.17.0 (2023-05-09): [[file:htmldoc_1_17_0/libgraph.html][library graph]], [[file:htmldoc_1_17_0/index.html][coqdoc presentation]] + + Version 1.16.0 (2023-02-01): [[file:htmldoc_1_16_0/libgraph.html][library graph]], [[file:htmldoc_1_16_0/index.html][coqdoc presentation]] + + Version 2.0+alpha1 (2022-12-05): [[file:htmldoc_2_0_alpha1/libgraph.html][library graph]], [[file:htmldoc_2_0_alpha1/index.html][coqdoc presentation]] + + Version 1.15.0 (2022-06-30): [[file:htmldoc_1_15_0/libgraph.html][library graph]], [[file:htmldoc_1_15_0/index.html][coqdoc presentation]] + + Version 1.14.0 (2022-01-19): [[file:htmldoc_1_14_0/libgraph.html][library graph]], [[file:htmldoc_1_14_0/index.html][coqdoc presentation]] + + Version 1.13.0 (2021-10-28): [[file:htmldoc_1_13_0/libgraph.html][library graph]], [[file:htmldoc_1_13_0/index.html][coqdoc presentation]] + + Version 1.12.0 (2020-11-26): [[file:htmldoc_1_12_0/libgraph.html][library graph]], [[file:htmldoc_1_12_0/index.html][coqdoc presentation]] + + Version 1.11.0 (2020-06-09): [[file:htmldoc_1_11_0/libgraph.html][library graph]], [[file:htmldoc_1_11_0/index.html][coqdoc presentation]] + + Version 1.10.0 (2019-11-29): [[file:htmldoc_1_10_0/libgraph.html][library graph]], [[file:htmldoc_1_10_0/index.html][coqdoc presentation]] +- The past stable releases of the Mathematical Components library + can be [[https://github.com/math-comp/math-comp/releases][downloaded from github]]. +- Older versions of the Mathematical Components library are also available: + + [[https://github.com/math-comp/math-comp/releases/tag/archive][historical archives]] (2008-2014) + + [[https://github.com/math-comp/mathcomp-history-before-github][pre-github archive]] diff --git a/index.html b/index.html index dace9d7d..02c65a6d 100644 --- a/index.html +++ b/index.html @@ -3,14 +3,14 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Mathematical Components - - + + @@ -199,81 +199,33 @@ - -
+

Mathematical Components

View the Project on GitHub

- -
-

About

-
+
+

About

+

Welcome to Mathematical Components' web-page!

Mathematical Components are libraries of formalized mathematics - developed using the Coq 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. +developed using the Rocq prover. 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.

-The libraries are written using the Ssreflect proof language, now part of -the standard distribution of the Coq proof assistant. +The libraries are written using the SSReflect proof language, now part of +the standard distribution of the Rocq prover.

@@ -282,102 +234,79 @@

About

- -
-

Get the library

-
+
+

Get the library

+
- - -
-

Documentation

-
+
+

Documentation

+
Mathematical Components book
- -
-

More material

-
+
+

More material

+
- - -
-

Help and contact

-
+
+

Help and contact

+
- -
-

Authors and contributors

-
+
+

Authors and contributors

+

-The Mathematical Components library and the Ssreflect proof language +The Mathematical Components library and the SSReflect proof language were initially developed by the Mathematical Components team at the Inria-Microsoft Research Joint Center. Today, the list of members of the Mathematical Components organization is visible here. diff --git a/index.org b/index.org index f7c43210..f1b67cf8 100644 --- a/index.org +++ b/index.org @@ -19,26 +19,22 @@ Welcome to Mathematical Components' web-page! Mathematical Components are libraries of formalized mathematics - developed using the [[http://coq.inria.fr][Coq]] 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. +developed using the [[https://rocq-prover.org/][Rocq]] prover. This project finds its roots +in the [[https://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf][formal proof of the Four Color Theorem]]. It has been used for +large scale formalization projects, including a formal proof of the +[[https://inria.hal.science/hal-00816699/document][Odd Order (Feit-Thompson) Theorem]]. -The libraries are written using the Ssreflect proof language, now part of -the standard distribution of the Coq proof assistant. +The libraries are written using the [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][SSReflect proof language]], now part of +the standard distribution of the Rocq prover. This is an open source project, licensed under the CeCILL-B free software license agreement. * Get the library -- The last stable releases of the Mathematical Components library +- [[file:installation.html][Installation instructions]] +- The source code of the Mathematical Components library can be [[https://github.com/math-comp/math-comp/releases][downloaded from github]]. -- [[file:installation.html][Installation instructions]]. -- Older versions of the Mathematical Components library are also available - ([[https://github.com/math-comp/math-comp/releases/tag/archive][historical archives]] (2008-2014), [[https://github.com/math-comp/mathcomp-history-before-github][pre-github archive]]) - * Documentation @@ -50,55 +46,42 @@ software license agreement. #+END_EXPORT -- The source file of each library features a documentation header - which describes the concepts and notations introduced in that library. +- A [[https://math-comp.github.io/mcb/][book]] that introduces the techniques for writing + algorithms and proofs and describes the design ideas of the + Mathematical Components library. -- The library graph can be explored interactively and the coqdoc - presentation of the source files can be browsed online: +- The library can be explored interactively and an HTML rendering of + the source code can be browsed online: + latest versions: * Version 2.5.0 (2025-10-13): [[file:htmldoc_2_5_0/libgraph.html][library graph]], [[file:htmldoc_2_5_0/index.html][coqdoc presentation]] * Version 2.4.0 (2025-04-14): [[file:htmldoc_2_4_0/libgraph.html][library graph]], [[file:htmldoc_2_4_0/index.html][coqdoc presentation]] * Version 2.3.0 (2024-11-28): [[file:htmldoc_2_3_0/libgraph.html][library graph]], [[file:htmldoc_2_3_0/index.html][coqdoc presentation]] - + older versions: * Version 2.2.0 (2024-01-17): [[file:htmldoc_2_2_0/libgraph.html][library graph]], [[file:htmldoc_2_2_0/index.html][coqdoc presentation]] - * Version 2.1.0 (2023-10-24): [[file:htmldoc_2_1_0/libgraph.html][library graph]], [[file:htmldoc_2_1_0/index.html][coqdoc presentation]] - * Version 2.0.0 (2023-05-10): [[file:htmldoc_2_0_0/libgraph.html][library graph]], [[file:htmldoc_2_0_0/index.html][coqdoc presentation]] - * Version 1.19.0 (2024-01-15): [[file:htmldoc_1_19_0/libgraph.html][library graph]], [[file:htmldoc_1_19_0/index.html][coqdoc presentation]] - * Version 1.18.0 (2023-11-01): [[file:htmldoc_1_18_0/libgraph.html][library graph]], [[file:htmldoc_1_18_0/index.html][coqdoc presentation]] - * Version 1.17.0 (2023-05-09): [[file:htmldoc_1_17_0/libgraph.html][library graph]], [[file:htmldoc_1_17_0/index.html][coqdoc presentation]] - * Version 1.16.0 (2023-02-01): [[file:htmldoc_1_16_0/libgraph.html][library graph]], [[file:htmldoc_1_16_0/index.html][coqdoc presentation]] - * Version 2.0+alpha1 (2022-12-05): [[file:htmldoc_2_0_alpha1/libgraph.html][library graph]], [[file:htmldoc_2_0_alpha1/index.html][coqdoc presentation]] - * Version 1.15.0 (2022-06-30): [[file:htmldoc_1_15_0/libgraph.html][library graph]], [[file:htmldoc_1_15_0/index.html][coqdoc presentation]] - * Version 1.14.0 (2022-01-19): [[file:htmldoc_1_14_0/libgraph.html][library graph]], [[file:htmldoc_1_14_0/index.html][coqdoc presentation]] - * Version 1.13.0 (2021-10-28): [[file:htmldoc_1_13_0/libgraph.html][library graph]], [[file:htmldoc_1_13_0/index.html][coqdoc presentation]] - * Version 1.12.0 (2020-11-26): [[file:htmldoc_1_12_0/libgraph.html][library graph]], [[file:htmldoc_1_12_0/index.html][coqdoc presentation]] - * Version 1.11.0 (2020-06-09): [[file:htmldoc_1_11_0/libgraph.html][library graph]], [[file:htmldoc_1_11_0/index.html][coqdoc presentation]] - * Version 1.10.0 (2019-11-29): [[file:htmldoc_1_10_0/libgraph.html][library graph]], [[file:htmldoc_1_10_0/index.html][coqdoc presentation]] - -- The Ssreflect language comes with a dedicated reference manual, - as a [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][chapter]] of Coq's reference manual. + + See [[file:history.html][this page]] for older versions. -- A [[https://math-comp.github.io/mcb/][book]] that introduces the techniques for writing - algorithms and proofs and describes the design ideas of the - library. +- The SSReflect proof language comes with a dedicated reference + manual, as a [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][chapter]] of Rocq's reference manual. -** More material +- Each file of the source code of the Mathematical Components library + features a documentation header which describes the concepts and + notations introduced in that file. -- [[file:documentation.html][Books, lectures, videos, etc.]] -- [[file:papers.html][Research papers]] related to Mathematical Components. Your paper or - thesis is not in the list? Send [[mailto:mathcomp-dev@inria.fr?subject=MathComp related paper][us]] a message to correct this. +** More material +- A selection of [[file:documentation.html][Books, lectures, videos, etc.]] +- [[file:papers.html][Research papers]] using the Mathematical Components library. + Send [[mailto:mathcomp-dev@inria.fr?subject=MathComp related paper][us]] a message or [[https://github.com/math-comp/math-comp.github.io][issue/PR on github]] to add any paper or thesis not in this list! * Help and contact -- Chat with us on [[https://coq.zulipchat.com/][Coq's Zulip]]! +- Chat with us on [[https://rocq-prover.zulipchat.com][Rocq's Zulip]]! (in particular via the ~math-comp~ channels) - Discuss with us on Coq's [[https://coq.discourse.group/][Discourse]] forum! -- [[mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect][Subscribe]] to the Ssreflect mailing list. +- [[mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect][Subscribe]] to the SSReflect mailing list (low volume). + Browse the [[https://sympa.inria.fr/sympa/arc/ssreflect][archives]] or consult the general [[https://sympa.inria.fr/sympa/info/ssreflect][information page]] of the mailing list. * Authors and contributors -The Mathematical Components library and the Ssreflect proof language +The Mathematical Components library and the SSReflect proof language were initially developed by the Mathematical Components team at the [[https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/][Inria-Microsoft Research Joint Center]]. Today, the list of members of the Mathematical Components organization is visible [[https://github.com/orgs/math-comp/people][here]]. diff --git a/installation.html b/installation.html index 4caa07da..7ae2e3fa 100644 --- a/installation.html +++ b/installation.html @@ -3,14 +3,14 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Mathematical Components: Installation - + @@ -199,55 +199,9 @@ - -

+

Mathematical Components: Installation

The Mathematical Components libraries are provided as separate packages: @@ -262,31 +216,31 @@

Mathematical Components: Installation

The installation of Mathematical Components is best done using opam, a -package manager for OCaml, the programming language with which Coq is -implemented. +package manager for OCaml, the programming language with which the +Rocq prover is implemented.

-The relevant packages can be found in the Coq package index; -their name is usually prefixed with coq-mathcomp-. +The relevant packages can be found in the Rocq package index; +their name is usually prefixed with rocq-mathcomp- or coq-mathcomp-.

- -
-

Install the Base Mathematical Components Libraries

-
+
+

Install the Base Mathematical Components Libraries

+
-
-

Installation using the opam package manager

-
+
+

Installation using the opam package manager

+
  • Using opam, the installation of the base Mathematical Components library is as simple as this:
-
-opam repo add coq-released https://coq.inria.fr/opam/released
+

+
opam repo add coq-released https://coq.inria.fr/opam/released
 opam install coq-mathcomp-ssreflect
 

+

 
 
    
 
  • Other base mathematical components libraries can then be installed
@@ -301,20 +255,18 @@ 
    Installation using the opa
- -
-

Installation using the Coq platform

-
+
+

Installation using the Coq platform

+
    -
  • The Coq platform is a distribution of Coq together with a selection of libraries +
  • The Coq platform is a distribution of Rocq together with a selection of libraries including most Mathematical Components libraries. It supports Linux, macOS, and Windows.
- -
-

Other installation instructions and details

-
+
+

Other installation instructions and details

+
  • You can find more detailed installation instructions in INSTALL.md (from the official distribution), this includes: @@ -340,10 +292,9 @@

    Other installation instructions and details

- -
-

Install Other Mathematical Components Libraries

-
+
+

Install Other Mathematical Components Libraries

+

There are several libraries that build on top of the base Mathematical Components libraries, e.g.: @@ -404,7 +355,7 @@

Install Other Mathematical Components Libraries

  • See the Mathematical Components' github.
    • -
  • coq-community also features a number of libraries using Mathematical Components.
    • +
  • rocq-community also features a number of libraries using Mathematical Components.
diff --git a/installation.org b/installation.org index c9c2d4ec..8d7da4c5 100644 --- a/installation.org +++ b/installation.org @@ -18,11 +18,11 @@ The Mathematical Components libraries are provided as separate packages: - 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 [[https://coq.inria.fr/][Coq]] is -implemented. +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://coq.inria.fr/opam/www/][Coq package index]]; -their name is usually prefixed with ~coq-mathcomp-~. +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 @@ -44,9 +44,9 @@ opam install coq-mathcomp-ssreflect + ~coq-mathcomp-fingroup~, + ~coq-mathcomp-character~. -** Installation using the [[https://github.com/coq/platform][Coq platform]] +** Installation using the [[https://github.com/rocq-prover/platform][Coq platform]] -- The [[https://github.com/coq/platform][Coq platform]] is a distribution of [[https://coq.inria.fr/][Coq]] together with a selection of libraries +- 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 @@ -97,5 +97,5 @@ Applications: More libraries: - See the Mathematical Components' [[https://github.com/math-comp][github]]. -- [[https://github.com/coq-community][coq-community]] also features a number of libraries using Mathematical Components. +- [[https://rocq-community.org/][rocq-community]] also features a number of libraries using Mathematical Components.