How are the Coq math-comp account and repositories related?
One of my side goals is to try to keep the tags on this site meaningful and useful.
Today I ran into this question:
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