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

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.

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

- Project code becomes maintained (e.g., in Coq-community GitHub org) and uses best practices for CI, does releases on opam
- Project becomes part of the Coq Platform (is accepted by Platform maintainers as having reached enough audience and quality)
- 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.

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

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

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.

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.

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

@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.

Yes, I would like to join this team.

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)

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

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.

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

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

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

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

Last updated: Jun 13 2024 at 07:01 UTC