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.

Done

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: Oct 08 2024 at 15:02 UTC