It seems more and more projects are using the `mathcomp`

tag on GitHub. This means we should probably create an "official" topic for this (compare https://github.com/topics/coq to https://github.com/topics/mathcomp). Here is the metadata required to create a topic, exemplified by Coq:

```
---
created_by: Gérard Pierre Huet, Thierry Coquand
display_name: Coq
github_url: https://github.com/coq/coq
logo: coq.png
released: 1989
short_description: Coq is a formal proof management system.
topic: coq
url: https://coq.inria.fr
wikipedia_url: https://en.wikipedia.org/wiki/Coq
---
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
```

Maybe MathComp devs help us out with what they think should be in the respective fields? In particular, what would count as the first release?

Could you explain what a topic is? It is a tag for searching? Any pointer would be great

@gares A topic is basically a small structured article associated with a GitHub tag.

@Enrico Tassi just compare the two links: https://github.com/topics/coq https://github.com/topics/mathcomp

this is basically about marketing (and the mini-description should be useful elsewhere, e.g., in a Wikipedia article)

btw, according to the GitHub rules creating a topic should be community driven

or even "must be", iirc

well, I'm not a MathComp dev

and this is mainly triggered by the many mathcomp-related projects in coq-community

I'm not saying you are :)))

It would be great to have more people adding "coq" / "mathcomp" / ... tags to their repos. So I try encouraging them by opening issues from time to time. Any help with that would be greatly appreciated.

@Enrico Tassi can we use this .png for `logo`

, or is there something else official? https://math-comp.github.io/mcb/cover-front-web.png

OK, I'm just going to throw this shallowly-researched data out there for corrections:

```
---
created_by: Georges Gonthier
display_name: Mathematical Components
github_url: https://github.com/math-comp/math-comp
logo: mathcomp.png
released: 2012
short_description: Extensive repository of formalized mathematical theories in Coq.
topic: mathcomp
url: https://math-comp.github.io
---
Mathematical Components is a repository 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.
```

Thanks, I'll bring this up for discussion at the next meeting: https://github.com/math-comp/math-comp/wiki/TopicsNextMeeting

there is even support for aliases, so `math-comp`

could be an alias for `mathcomp`

(which will not happen without the official topic, to my knowledge)

Karl Palmskog said:

there is even support for aliases, so

`math-comp`

could be an alias for`mathcomp`

(which will not happen without the official topic, to my knowledge)

Yes, such an alias would be nice. Just because of the mismatch between (and within) URLs like https://github.com/math-comp/math-comp/tree/master/mathcomp and the packages `coq-mathcomp-something`

. :grimacing:

for those following this, my `mathcomp`

GitHub topic PR was recently merged: https://github.com/github/explore/pull/1943

However, the curation has not yet appeared on GitHub (hopefully soon): https://github.com/topics/mathcomp

they finally rolled out the `mathcomp`

topic!

https://github.com/topics/mathcomp

Just in case someone wonders: the picture is so tiny because... you have no choice ;-)

in the future, all code/content we see will be dictated by someone's nitpicky CI

reminder that https://github.com/math-comp/math-comp/issues/616 can now be closed

Last updated: Jul 23 2024 at 21:01 UTC