Théo Zimmermann (Nov 24 2020 at 18:32): Théo Zimmermann (Nov 24 2020 at 18:32):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.
Andrew Miloradovsky (Nov 24 2020 at 20:35):@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.
Karl Palmskog (Nov 24 2020 at 20:37):@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
Karl Palmskog (Nov 24 2020 at 22:00):moreover, this may be a good opportunity to merge the projects into a single repo (they can still have separate packages)
Théo Zimmermann (Nov 25 2020 at 08:15):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.
Karl Palmskog (Nov 25 2020 at 08:57):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, _CoqProject.proj1, _CoqProject.proj2. Dune solves this, but without 1.0 release shouldn't be viewed as a solution for the opam archive.
Karl Palmskog (Nov 25 2020 at 09:04):anyway, I would advocate merging the sources of Zorn's Lemma into Topology, and marking the former as archived.
Karl Palmskog (Nov 25 2020 at 09:04):maybe after a final synchronized release of both
Karl Palmskog (Nov 25 2020 at 09:05):I think we are anyway spread too thin among projects in the Coq world, even though tooling is not exactly optimized for monorepo
Karl Palmskog (Nov 25 2020 at 09:19):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
Stéphane Desarzens (Dec 19 2020 at 21:31):Hi everyone.
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.
Karl Palmskog (Dec 20 2020 at 07:54):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:
Karl Palmskog (Dec 20 2020 at 07:55):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.
Stéphane Desarzens (Dec 20 2020 at 13:50):Ok, if you think it's feasible.
Karl Palmskog (Dec 21 2020 at 09:05):@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 theories/sets and theories/topology?
Karl Palmskog (Dec 21 2020 at 09:06):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
Théo Zimmermann (Dec 21 2020 at 09:11):If we wish to preserve commit history, then some git subtree magic might do it.
Karl Palmskog (Dec 21 2020 at 09:16):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
Karl Palmskog (Jan 11 2021 at 19:31):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