Stream: coq-community devs & users

Topic: Maintenance status of zorns-lemma and topology


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 25 2020 at 09:04):

maybe after a final synchronized release of both

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Stéphane Desarzens (Dec 20 2020 at 13:50):

Ok, if you think it's feasible.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 09:11):

If we wish to preserve commit history, then some git subtree magic might do it.

view this post on Zulip 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

view this post on Zulip 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: Feb 05 2023 at 13:02 UTC