I just opened issue https://github.com/coq-community/manifesto/issues/139 in coq-community.
This is a ping to one of the math-comp organization owners @Cyril Cohen, @Enrico Tassi, @Assia Mahboubi, @Maxime Dénès to perform the github operation : go in the danger zone and press on the relevant button. I personnally don't have the right to do so. If I remember well, it was agreed in meeting yesterday that Cyril would do it.
(I assume this is about moving
fourcolor repo to the
coq-community GitHub organization)
I don't understand the behavior of zulip here. Thanks for moving the message at the right place.
I didn't know Cyril was doing the move, otherwise would have pinged him, sorry for the noise Yves.
Until yesterday, I did not know I was unable to do it, so it was natural that you ping me.
I can do it rightaway if @Cyril Cohen is away.
This could be an opportunity for some PR via Twitter if someone with control of a widely followed account feels up to it. My suggestion is something like:
The formal proof in Coq of the four color theorem by Georges Gonthier has found a new home in Coq-community on GitHub, where it will be collaboratively maintained for the long term (https://github.com/coq-community/fourcolor). The project is already an optional dependency of the graph theory library in Coq-community (https://github.com/coq-community/graph-theory).
Last updated: Jun 01 2023 at 13:01 UTC