Stream: coq-community devs & users

Topic: Meta-project to consolidate Coq libraries

Karl Palmskog (Dec 10 2022 at 11:47):

As part of development of Hydras & Co, we recently transferred results into CoqPrime as a way to consolidate dependencies related to the Gödel incompleteness proof.

I think we need more consolidation efforts like this to address the fragmentation of generic Coq code into many separated silos. We might consider starting a meta-project of sorts to lead Coq-community projects toward consolidation, in particular into libraries that are part of the Coq Platform (https://github.com/topics/coq-platform)

Maybe a meta-issue is appropriate in the manifesto repo? I had one specific issue in the meantime: https://github.com/coq-community/bertrand/issues/18

Andres Erbsen (Dec 10 2022 at 14:50):

I think this is a very valuable goal and I am interested in helping. I am especially interested in consolidating results that would qualify for inclusion in the standard library once cleaned up. Modular arithmetic, finite maps, and sorting are perhaps the clearest cases where grafting a common-denominator implementation and theory from popular developments would greatly improve the standard library.

Karl Palmskog (Dec 10 2022 at 14:54):

@Andres Erbsen I think our general pipeline is something like this:

1. Project code becomes maintained (e.g., in Coq-community GitHub org) and uses best practices for CI, does releases on opam
2. Project becomes part of the Coq Platform (is accepted by Platform maintainers as having reached enough audience and quality)
3. Project as whole or in part is integrated into Stdlib

I personally don't see 3. as high priority, since we are pushing the Platform these days rather than Coq itself, e.g., coq-stdlib in 8.17 is "just" an opam package.

Karl Palmskog (Dec 10 2022 at 14:56):

recent example, where for me personally as co-maintainer the Platform membership is enough: https://github.com/coq-community/coq-mmaps

Andres Erbsen (Dec 10 2022 at 15:00):

I guess this is yet again a case of differing visions for the Coq ecosystem, but at least our goals are compatible.

Karl Palmskog (Dec 10 2022 at 15:09):

since there was some interest, I created the Coq-community manifesto repo issue where we could track consolidation issues: https://github.com/coq-community/manifesto/issues/143

I don't mind if something goes into Stdlib, but just not a priority, so goals should be compatible, yes.

Théo Zimmermann (Dec 10 2022 at 15:11):

Some people have been considering for a while (most recently @Ali Caglayan) that splitting the coq-stdlib to a separate repo could be beneficial to its maintenance by interested stakeholders. In the same spirit, it could be divided into a set of well-thought and consistent packages that, consolidated with other well-thought and consistent packages from the Coq Platform, could become what is branded as "Coq's standard library". E.g., this could be a subset of the "full tier" of the Coq Platform with some stricter inclusion criteria. Anyway, that's just some food for thought for the long-term. For the short / medium-term, I wholeheartedly support the project proposed here.

Karl Palmskog (Dec 10 2022 at 15:12):

I guess we could even track small things, like there are several lemmas in AAC Tactics which have "submit to Stdlib" TODOs

Karl Palmskog (Dec 10 2022 at 15:18):

@Andres Erbsen by the way, have you thought about joining the Stdlib-maintainers Coq GitHub team (https://github.com/orgs/coq/teams/stdlib-maintainers)? From what I could see, that team was seemingly lacking in manpower, and it might help the consolidation effort to strengthen it.

Andres Erbsen (Dec 10 2022 at 15:19):

Yes, I would like to join this team.

Karl Palmskog (Dec 10 2022 at 15:22):

and also, based on Andres's feedback in the issue, I think we in Coq-community can also try to coordinate consolidation not directly related to Coq-community projects (to a reasonable degree, we don't really want to stray too far into projects other people maintain)

Karl Palmskog (Dec 10 2022 at 15:32):

@Théo Zimmermann could you add Andres to the Stdlib-maintainers team?

Théo Zimmermann (Dec 10 2022 at 15:35):

Done. @Andres Erbsen Please read carefully the documentation at https://github.com/coq/coq/blob/master/CONTRIBUTING.md#becoming-a-maintainer, and more specifically at https://github.com/coq/coq/blob/master/CONTRIBUTING.md#merging-pull-requests about your newfound powers.

Karl Palmskog (Dec 10 2022 at 15:36):

if you want to try out the process, my small Stdlib PR happens to be available: https://github.com/coq/coq/pull/16926

Karl Palmskog (Dec 10 2022 at 15:37):

(incidentally, that PR was also about consolidation from another Coq project I co-maintain)

Andres Erbsen (Dec 10 2022 at 16:26):

:thumbs_up: Indeed, looks like I'm landing right in the middle of compatibility discussion too :).

Bas Spitters (Dec 11 2022 at 20:14):

I've added some candidates here: https://github.com/coq-community/manifesto/issues/143#issuecomment-1345649198

Last updated: Jun 03 2023 at 18:01 UTC