Explanation of Coq math-comp repositories

Question

How are the Coq math-comp account and repositories related?

---

Details

One of my side goals is to try to keep the tags on this site meaningful and useful.

Today I ran into this question:

How to prove has_esp when using mathcomp.analysis?

I do not use Coq so take that in mind.

When I saw

Page of mathcomp.analysis: https://github.com/math-comp/analysis

I thought it was odd as the tag coq-mathcomp was used, but then a specific repository was given. In looking at at the mathcomp account (https://github.com/math-comp), which is different from the matchcomp repository (https://github.com/math-comp/math-comp) I did see a separate repository for analysis (https://github.com/math-comp/analysis).

I know that sometimes that with GitHub accounts multiple repositories can be loaded into a tool by various means with a package management system being common.

I also downloaded the code as noted on the web page (https://github.com/math-comp/math-comp/releases) and searched for an analysis directory and found none thinking that analysis would be included in the download on the web page.

So it seems that some useful information is glossed over on the web page.

My current thought to my question above is

• math-comp/math-comp - What most users mean when the mention Coq and math-comp
• math-comp/analysis - Analysis code not installed with math-comp/math-comp
• math-comp/algebra-tatics - Another repository not installed with math-comp/math-comp
• math-comp/math-comp.github.io - The website https://math-comp.github.io/

...

Needless to say for those that use it often, it is not confusing, but to some one new it is as confusing as the different Lean accounts. (ref)

The primary goal of this question is to have an answer that makes it clear to some one not familiar with Coq math-comp account and repositories to understand what they need to install, be it one of the repositories or a combination of them.

Using that answer, it should be clear enough to know how to add tags related to math-comp as they are needed. That does not need to be addressed in the answer, but it will be used as a criteria for accepting an answer.

---

Note: For the question How to prove has_esp when using mathcomp.analysis?, I created, added and edited the tag coq-mathcomp-analysis

Answer 1

As Meven wrote, the Mathematical Components repositories originate from the work of Georges Gonthier and his team proving first the Four Color Theorem, then the Odd Order Theorem.

In Coq people do not install "repositories", they install "packages" (most often through the opam package manager, but this can also be through the Nix package manager or through a distribution like Debian). The MathComp library contained in the main repository (math-comp/math-comp) is already divided into multiple packages:

• coq-mathcomp-algebra
• coq-mathcomp-character
• coq-mathcomp-field
• coq-mathcomp-fingroup
• coq-mathcomp-ssreflect

But there are many more packages that have the coq-mathcomp- prefix and are also available to users. These packages are developed in separate repositories (most of them under the math-comp organization, but now the fourcolor repository has migrated to the coq-community organization).

Roughly speaking, the criteria for a package to be inside or outside the main repository is supposed to be its quality and maturity, but also its reusability (that's why odd-order and fourcolor are outside).

All of these packages and the ones that depend on them form what one could call the "MathComp sub-ecosystem of the Coq ecosystem".

Answer 2

Roughly, Mathematical Components are a set of libraries that are designed to work together, and follow a lot of common ideas and guidelines, in particular the use of the SSReflect proof language, which is a dialect of Coq. It takes its root in the proof of the Four Color Theorem by the team around Georges Gonthier.

The main library is the math-comp one, which contains a lot of "basic" formalizations, mainly regarding mathematical structures (groups, rings, fields, and so on). This serves as the main base for other formalization projects, the main one being the proof of the Odd Order Theorem (repo odd-order), and an experimental library for analysis (repo analysis).

It has also strong ties to tools such as Hierarchy Builder (which aims at automating the build of hierarchies of structures, such as the one which serves as the backbone of math-comp), or the tactics developed in algebra-tactics.

Finally, there’s also the source of a book presenting some ideas around the libraries (repo mcb), and the website of the organization (math-comp.github.io).