Karl Palmskog (Apr 21 2022 at 12:40): Karl Palmskog (Apr 21 2022 at 12:40):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?
Théo Zimmermann (Apr 21 2022 at 12:46):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).
Théo Zimmermann (Apr 21 2022 at 12:47):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.
Karl Palmskog (Apr 21 2022 at 12:49):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
Théo Zimmermann (Apr 21 2022 at 12:51):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.
Karl Palmskog (Apr 21 2022 at 12:54):OK, I trust you will figure it out inside core then, if something goes more awry than before
Michael Soegtrop (Apr 21 2022 at 13:20):And on top comes the single RM for Coq Platform ... so two chain links which can fail.
Karl Palmskog (Apr 21 2022 at 13:23):I think the Platform RM tasks could at least become more automated over time. For the Coq RM, how automatable is that even?
Théo Zimmermann (Apr 21 2022 at 13:24):This could also become more automated over time.
Karl Palmskog (Apr 21 2022 at 13:33):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]
Karl Palmskog (Apr 21 2022 at 13:35):yet, from ecosystem standpoint, more automation is nice
Michael Soegtrop (Apr 21 2022 at 14:34):@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.
Karl Palmskog (Apr 21 2022 at 14:39):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: Oct 12 2024 at 13:01 UTC