Stream: math-comp users

Topic: GitHub topic for mathcomp


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Anton Trunov (Oct 13 2020 at 11:50):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Oct 13 2020 at 11:52):

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

view this post on Zulip Anton Trunov (Oct 13 2020 at 11:52):

or even "must be", iirc

view this post on Zulip Karl Palmskog (Oct 13 2020 at 11:53):

well, I'm not a MathComp dev

view this post on Zulip Karl Palmskog (Oct 13 2020 at 11:53):

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

view this post on Zulip Anton Trunov (Oct 13 2020 at 11:53):

I'm not saying you are :)))

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 13 2020 at 12:40):

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

view this post on Zulip 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)

view this post on Zulip Christian Doczkal (Oct 13 2020 at 15:51):

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:

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 01 2020 at 07:13):

they finally rolled out the mathcomp topic!

https://github.com/topics/mathcomp

view this post on Zulip Enrico Tassi (Dec 01 2020 at 19:10):

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

view this post on Zulip Karl Palmskog (Dec 01 2020 at 20:12):

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

view this post on Zulip 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: Jan 29 2023 at 19:02 UTC