search

coq-community / topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Other
46 stars 10 forks source link

Move set-theoretic lemmas to zorns-lemma #14

Closed Columbus240 closed 3 years ago

Columbus240 commented 3 years ago

To develop topology we need many facts from set theory. For this the zorns-lemma library was initially developed. There are currently quite a few lemmas about sets (i.e. Ensembles) in the topology library, that could as well go into zorns-lemma.

I think it’d be "cleaner" if the facts & tactics about logic & set-theory that don’t depend on topological notions were moved to zorns-lemma. EnsembleTactic.v, InverseImageLemmas.v and the finite_indexed_union in SumTopology.v come to my mind. If the current maintainers are ok with that, I’d copy the code mentioned above into zorns-lemma. I’d only remove the code here if the PR in zorns-lemma is accepted.

But this would only "fix" the current state. What if the topology library needs more set theory that hasn’t been developed yet in zorns-lemma? Every time we develop the new set-theoretic fact we would have to move it to zorns-lemma first, before we could commit the topologic fact depending on it... I’m not yet sure about that. I think it would be a "nice" policy for this repo to have, but I’m not yet sure whether it is practical. What do you think?

palmskog commented 3 years ago

@Columbus240 it sounds like a good idea to me to factor out more pure set theory results to the zorns-lemma library (@stop-cran hopefully agrees).

The best approach may to be first "duplicate" the set theory results in zorns-lemma and then remove them from topology. Hence, the initial work is likely best done in the zorns-lemma project. However, the main maintainer of zorns-lemma said he will not have time to work on that project for a while. @Columbus240 are you interested in co-maintaining the zorns-lemma repo? I can help set that up if so.

Zimmi48 commented 3 years ago

In this Zulip thread, we discussed that it would make sense to merge the two projects in a single "mono-repository". The tooling is not yet fully ready for this but Dune should still make this possible, and this would ease the transfer of lemmas from one library to the other.

BTW, following this discussion, I also thought that we'd asked @stop-cran to co-maintain both repositories (IMHO it makes sense to keep the same team of maintainers on both, since they generally interest the same people).

stop-cran commented 3 years ago

@Zimmi48 I think I can help in maintaining zorns-lemma as well.

Columbus240 commented 3 years ago

I’d be happy to work more on topology (& zorns-lemma). But what responsibility would I have as co-maintainer? (I read the coq-community/manifesto) It may happen that I don’t login to Github for some months or that I don’t check the associated mailbox for a while. So it might take a while until I answer any issues or pull requests. Would that be ok?

I’m also not so sure in which direction I’m allowed develop these libraries. There are many topics or theorems that may be added, or changes to the style of proofs that might be done. I find the current style often very hard to follow, since it often omits bullet points. Are there expectations in what directions the development should go or shouldn’t go?

I’d be happy to have a chat on some medium (here, Zulip, something else?) about this.

Edit: Of course I should add, that I work on/with topology & zorns-lemma only in my free time and would like to keep it that way. So I can’t strictly guarantee any work. But I’m sure my interest in Coq and the mathematics involved will make me do something. ;)

palmskog commented 3 years ago

The main formal responsibility of a maintainer is to respond to (somehow act on, not necessarily merge) incoming pull requests - this is elaborated on here. Responsibilities can be delegated, so it's not necessary for one particular person to respond to a PR quickly. Maintainers can also step down at any time if they wish.

A secondary informal responsibility is to maintain compatibility with new released Coq versions, and ideally even the development Coq version. Many maintainers also think about evolving their projects to better suit the community's needs (submit their own PRs), but this is far from a requirement. The members of coq-community are volunteers and most work on their free time.

Zulip is indeed the best place for casual questions and chat.

Columbus240 commented 3 years ago

Sounds good to me.

Columbus240 commented 3 years ago

The whole file Filter.v can also be moved to zorns-lemma, but I’ll do that after the repos have merged.

Zimmi48 commented 3 years ago

I've added @Columbus240 to the list of maintainers in the description of the repository, but the meta.yml and (auto-generated) README.md will have to be fixed as well.

Columbus240 commented 3 years ago

Closing, since all things mentioned above have been moved from Topology to ZornsLemma.