Stream: math-comp devs

Topic: Coq-community MC overlay mergers


view this post on Zulip Karl Palmskog (Dec 05 2023 at 12:41):

Since we have quite a few MathComp CI projects in Coq-community, I've added specific GitHub org team "MathComp Overlay mergers" that have access to merge MC overlay PRs. Currently, this team has Pierre and Cyril as members, but we can update it whenever convenient - should it have other/more people, or how/when are overlays handled in MC?

view this post on Zulip Karl Palmskog (Dec 05 2023 at 12:43):

(one of the points of Coq-community is that we should never be "stuck" with overlay merges either for Coq or MC, which I guess have happened for Coq in the past)

view this post on Zulip Pierre Roux (Dec 05 2023 at 13:31):

I guess we can add Enrico (@gares on github), Kazuhiko (@pi8027) and Reynald (@affeldt-aist) at least (looking at recent mergers).

view this post on Zulip Pierre Roux (Dec 05 2023 at 13:33):

Overlay handling in MC remains quite artisanal, no strict rule. Since they are often backward compatible it's not uncommon that overlays are merged directly by the PR author and not even formalized as overlays in the CI.

view this post on Zulip Karl Palmskog (Dec 05 2023 at 14:07):

@Reynald Affeldt I invited you as a member of Coq-community to let you join the MC CI maintainer team

view this post on Zulip Reynald Affeldt (Dec 05 2023 at 14:18):

Hi @Karl Palmskog ! Got it. I'll do my best to be operational ASAP.

view this post on Zulip Karl Palmskog (Dec 05 2023 at 14:29):

great! just be to extra clear, being in this team should require minimal work for members, we just hope to host more MC CI projects in the future and this could make it a bit smoother


Last updated: Jul 23 2024 at 21:01 UTC