Stream: coq-community devs & users

Topic: Sister organizations on GitHub


view this post on Zulip Karl Palmskog (Mar 15 2022 at 13:04):

We may want to track sister organizations on GitHub over time to see what they are doing:

view this post on Zulip Théo Zimmermann (Mar 15 2022 at 17:44):

How do you define what makes a sister organization? If you use our CPMO (Community Package Maintenance Organization) definition (https://hal.inria.fr/hal-03320556), some of the ones you listed are a bit fringe because they do not document any process for adding packages or even new members. And here are a few more that we know about:

Here are a few more that we initially thought qualified but eliminated in the end:

view this post on Zulip Alexander Gryzlov (Mar 15 2022 at 17:48):

Idris has semi-official https://github.com/idris-community/

view this post on Zulip Alexander Gryzlov (Mar 15 2022 at 17:50):

also I should note that Typelevel doesn't cover the full Scala community, even in the FP subset there's also https://github.com/zio which is sort of a competing sub-community

view this post on Zulip Karl Palmskog (Mar 15 2022 at 18:07):

"sister organization" was just a vague way of saying "is a bit like coq-community". In the case of Lean, since they go nearly all in on monorepo, there is probably no need to document a process for adding packages.

view this post on Zulip Karl Palmskog (Mar 15 2022 at 18:09):

it's interesting that Scala has competing subcommunities. I guess we could view the "MPI community" (Iris, stdpp, ...) in this way, sort of. But thanks to the Platform and Coq package index, there is at least a way to intermingle packages

view this post on Zulip Théo Zimmermann (Mar 15 2022 at 18:10):

Isn't autosubst kind of MPI community-related and yet in coq-community?

view this post on Zulip Karl Palmskog (Mar 15 2022 at 18:11):

not exactly, since it originated in a non-MPI setting (Saarland university). It happens to be currently maintained by someone affiliated to MPI (Ralf)

view this post on Zulip Karl Palmskog (Mar 15 2022 at 18:12):

however, there are obviously ties between MPI-SWS and Saarland university, I believe MPI-SWS get all their students degrees via Saarland

view this post on Zulip Karl Palmskog (Mar 15 2022 at 18:16):

I like how Typelevel (and also Zio) explicitly say that they maintain generally useful stuff. I guess we could be clearer that quite a lot of our projects are generally useful to Coq users, although it's not a requirement.

view this post on Zulip Paolo Giarrusso (Mar 15 2022 at 19:24):

well, in a technical sense zio is competing with typelevel like math-comp is "alternative" to stdpp etc. — they're opinionated ecosystems.

view this post on Zulip Karl Palmskog (Mar 15 2022 at 19:45):

it's probably useful to classify "openness" of an organization in several dimensions like:

I presume Théo has already thought about this somewhere.


Last updated: Feb 05 2023 at 14:02 UTC