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-compcould 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
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
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: Jan 29 2023 at 19:02 UTC