Sorry if I don't follow Coq dev and Coq calls, but will it be the default to have a single RM going forward?
From ecosystem standpoint, I worry that if something unforeseen happens to the RM (illness, traveling with short notice, etc.), there is no backup plan. Or is there?
I agree with the worry, but the reality is that most recent releases have been managed by a single RM in practice (Guillaume was twice alone, Enrico was supposed to be assisted by Maxime but alone in reality, Pierre-Marie was supposed to be assisted by Matthieu but alone in practice). I think the only recent exception was when we managed the 8.12 release with Emilio. We really worked together on it (even though I managed the backporting process alone).
And your worry is really on point given that we had several releases delayed because the RM was too busy by something else or didn't communicate sufficiently clearly what he expected from other devs.
right, we have several versions of single-RM-in-practice. I guess I was hoping for that the co-RM would become a form of "RM-on-call", i.e., core would not need to go through an election process if there was a need for a replacement
That's an interesting idea, although the "on-call" concept might be difficult to put in practice given that finding one RM for a release is already difficult.
OK, I trust you will figure it out inside core then, if something goes more awry than before
And on top comes the single RM for Coq Platform ... so two chain links which can fail.
I think the Platform RM tasks could at least become more automated over time. For the Coq RM, how automatable is that even?
This could also become more automated over time.
was it Paolo who pointed out that "automatable" is in some sense in conflict with desirability of a task? If you do something automatable, it could be argued that you're doing something unnecessary [since it's going to be taken care of by systems soon]
yet, from ecosystem standpoint, more automation is nice
@Karl Palmskog : the basics are already fairly automated, say the generation of the "please tag" issues. But it is still quite a bit of work, say packages like quickchick or hammer. This needs active management to be usable in a cross platform environment.
I'm not sure QuickChick or CoqHammer are going to be the main issues. The whole Coq release process is like a marathon relay race (many people picking up batons and passing them on after some time). If more than a few batons are missed, the whole process could be delayed and in the worst case come to a halt
Last updated: May 31 2023 at 16:01 UTC