Hi @Andrew Miloradovsky, what is your current commitment with respect to the two coq-community projects zorns-lemma and topology? Would you like to keep being a maintainer for them or to step down? Would you like to have a co-maintainer? There are a couple of PRs on each of these projects that have not received any answer. If you'd like to step down or get a co-maintainer, maybe we should ask to
@stop-cran, who has contributed quite a lot to these two projects.
@Théo Zimmermann Sorry, I won't be able to contribute to the projects until at least the end of the year, maybe longer. My mind is currently in a completely different context. I haven't lost the interest, but recently I couldn't afford to spend any substantial time with Coq either. So, yes, at least a co-maintainer is needed, and @stop-cran indeed seems like a good candidate.
@Théo Zimmermann it sounds then like we will create a maintainer-wanted issue for the repo and then see if stop-cran is interested. In the meantime, we can fix the Travis issues, etc., in particular, I will take care of PR https://github.com/coq-community/zorns-lemma/pull/7 which needs updating
moreover, this may be a good opportunity to merge the projects into a single repo (they can still have separate packages)
Thanks for your answer Andrew, and thanks for your help Karl! Indeed, I agree that the two projects should probably be merged into a single repo. People who have expressed interest are usually interested in both.
one annoying issue with monorepo for several independent projects is that coq_makefile's
make install will not work as expected, it demands a "common root" of projects in the file listing. So to use coq_makefile, one will have to repeat file listings, e.g.,
_CoqProject.proj2. Dune solves this, but without 1.0 release shouldn't be viewed as a solution for the opam archive.
anyway, I would advocate merging the sources of Zorn's Lemma into Topology, and marking the former as archived.
maybe after a final synchronized release of both
I think we are anyway spread too thin among projects in the Coq world, even though tooling is not exactly optimized for monorepo
we need to support stuff like this in the templates as well, but with inter-project dependencies: https://github.com/coq-community/hydra-battles/pull/11/files
Do "we" even want to keep the opam packages of zorns-lemma and topology separate? When we do a monorepo, we might as well treat it as a single opam package. I don’t think many people depend on the packages being separate. Even though I think it’d be really nice to have separate opam packages and repos. Since only so few (~10 if we’re generous) people are involved with these libraries, separate repos (& opam packages) add to the administrative effort while giving (as far as I could tell) only "conceptual/abstract" benefits.
in general, we want to maximize potential for reuse of packages, and big packages that include both general collections of libraries and specific special-interest results will not be as interesting to the community as well-sliced packages. Compare:
so even if a monorepo is made out of Zorn's Lemma and Topology, I don't think they should be a single package. Since effort was made to conceptually separate them, I think there is value there that should be preserved.
Ok, if you think it's feasible.
@Théo Zimmermann do you have an opinion about how to best merge repos? Seems hard to preserve history fully in topology. I guess we follow hydra-battles and do something like
since packages are not independent I don't see a good alternative to what I did in Chapar for CI: https://github.com/coq-community/chapar/blob/master/.github/workflows/docker-ci.yml
If we wish to preserve commit history, then some
git subtree magic might do it.
I think one nice property would be if one could trace the edit history of a Zorn's lemma file all the way back, and
git subtree might make that possible
nice to see that cool stuff seems to be happening in https://github.com/coq-community/topology now...
Last updated: Jun 03 2023 at 18:01 UTC