search

coq-community / topology

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

Modernizing for Coq 8.7+ #1

Closed amiloradovsky closed 5 years ago

amiloradovsky commented 6 years ago

I still didn't manage to fix the Tietze extension theorem, but nothing else seems to depend on it in this repository.

See also https://github.com/coq-contribs/zorns-lemma/pull/1

herbelin commented 5 years ago

Thanks a lot. I merged your commits 1, 2, 3, 6, and the addition of bullets in 7. I skipped commit 4 (adding path to zorns-lemma) which assumes a layout which has no reason to be same for everyone. We unfortunately both changed master independently, so I skipped commit 5 which was conflictual (in RationalsInReals.v) and one line in commit 7.

Side question: would you be interested in moving zorns-lemma and topology to coq-community (and, optionally, be the official current maintainer)?

amiloradovsky commented 5 years ago

You mean https://github.com/coq-community. — Yes, I think I am interested. What is the procedure?

herbelin commented 5 years ago

@Zimmi48 will correct me if I'm wrong, but I think I just need your ok and then click somewhere to move the repository from here to coq-community. Then, you'll be the maintainer for as long as you want, especially in charge of merging PRs if any, coordinating discussions about PRs if needed, contributing extensions if you wish, proposing collaborative projects around the work, if relevant.

Zimmi48 commented 5 years ago

Indeed, this is as simple as this, although an additional good first step would be to open an issue at https://github.com/coq-community/manifesto/issues because this will give some publicity to the move.

Zimmi48 commented 5 years ago

@amiloradovsky: would you like me to proceed with the transfer to coq-community and adding you as the maintainer there?

amiloradovsky commented 5 years ago

@Zimmi48 Yes, please.

I was a little busy the last couple weeks. And I'll be away from my main machine(s) for yet another week or so. But generally I have plans regarding integration of some further theory.

Zimmi48 commented 5 years ago

@amiloradovsky Sorry for the long delay: I have opened https://github.com/coq-community/manifesto/issues/43. Can you confirm there that you are still interested in taking over as official maintainer?