Karl Palmskog (Oct 13 2020 at 11:17): Karl Palmskog (Oct 13 2020 at 11:17):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?
Enrico Tassi (Oct 13 2020 at 11:49):Could you explain what a topic is? It is a tag for searching? Any pointer would be great
Anton Trunov (Oct 13 2020 at 11:50):@gares A topic is basically a small structured article associated with a GitHub tag.
Karl Palmskog (Oct 13 2020 at 11:51):@Enrico Tassi just compare the two links: https://github.com/topics/coq https://github.com/topics/mathcomp
Karl Palmskog (Oct 13 2020 at 11:52):this is basically about marketing (and the mini-description should be useful elsewhere, e.g., in a Wikipedia article)
Anton Trunov (Oct 13 2020 at 11:52):btw, according to the GitHub rules creating a topic should be community driven
Anton Trunov (Oct 13 2020 at 11:52):or even "must be", iirc
Karl Palmskog (Oct 13 2020 at 11:53):well, I'm not a MathComp dev
Karl Palmskog (Oct 13 2020 at 11:53):and this is mainly triggered by the many mathcomp-related projects in coq-community
Anton Trunov (Oct 13 2020 at 11:53):I'm not saying you are :)))
Anton Trunov (Oct 13 2020 at 11:56):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.
Karl Palmskog (Oct 13 2020 at 11:59):@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
Karl Palmskog (Oct 13 2020 at 12:11):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
Karl Palmskog (Oct 13 2020 at 12:42):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)
Christian Doczkal (Oct 13 2020 at 15:51):Karl Palmskog said:
there is even support for aliases, so
math-compcould be an alias formathcomp(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:
Karl Palmskog (Nov 10 2020 at 11:11):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
Karl Palmskog (Dec 01 2020 at 07:13):they finally rolled out the mathcomp topic!
https://github.com/topics/mathcomp
Enrico Tassi (Dec 01 2020 at 19:10):Just in case someone wonders: the picture is so tiny because... you have no choice ;-)
Karl Palmskog (Dec 01 2020 at 20:12):in the future, all code/content we see will be dictated by someone's nitpicky CI
Karl Palmskog (Dec 07 2020 at 11:10):reminder that https://github.com/math-comp/math-comp/issues/616 can now be closed
Last updated: Apr 19 2024 at 21:01 UTC