{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7042","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7042/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7042/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7042/events","html_url":"https://github.com/coq/coq/issues/7042","id":307604519,"number":7042,"title":"What does time for discussion mean?","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":5,"created_at":"2018-03-22T11:28:34Z","updated_at":"2018-03-22T16:04:54Z","closed_at":null,"author_association":"OWNER","body":"I'm opening this issue to centralize a discussion started at #7023 and which has no reason to be continued there.\r\n\r\nSummary: in the last few years, it has been made clear at various occasions that communication targetting the whole development team was expected so that the opinions, suggestions, needs of everyone in the team could be taken into account whenever wanted. (*)\r\n\r\nIn the period when @maximedenes was merging PRs, it has been made clear (e.g. #5986) that both predictability of when a PR is merged was important and that a more \"agile\" merging which a single person is not able to give was necessary.\r\n\r\nWith the new merging process, we have an opportunity to improve on both issues: being more agile by distributing the process, being more structured in the protocol we use. And we have actually no choice than being more structured so that every \"merger\" knows clearly how to proceed in a way which is consensual.\r\n\r\nTo satisfy the need for a clear communication (*), which, again, various events show in the past that this is required for everyone in the team to feel his words and needs respected, the option that I'm proposing is to put some temporal guidelines to frame our discussions, as it is common to do in many collective processes (see also Robert which @silene mentioned at some time).\r\n\r\nI'm not saying that we need to have a heavy frame and the lighter it shall be, the best it shall be. I'm only saying that we need to give time and space to enough discussions so that anyone can feel that his/her opinion is admissible if there is one, as several of us already asked in the past.\r\n\r\nFor instance, a light way to proceed in situations like #7023 would be that running the merging script starts a daemon that shall merge the PR after 24h and add a comment of the following form to the PR discussion: \"Merging will be processed in 24h. If you see anything wrong with this PR and want to add something, it shall be more convenient that you do it in the next hours than later on\" (or any other formulation which everyone would feel comfortable with). \r\n\r\nLet me now answer to some comments posted at #7023:\r\n\r\nFrom @maximedenes:\r\n> > the question of minimal/maximal time has been asked several times and we shall not escape to eventually address it\r\n> \r\n> It has been addressed many times in working groups after you raised it, and the answer was, as I understood it, \"no fixed minimal delay\".\r\n\r\nYou are not answering to my question. My question is: \"where do you leave explicit time for discussion\", a time for discussion which you were among those to ask several times in the past regarding my own PRs, even for bug fixes.\r\n\r\nFrom @maximedenes:\r\n> That's too heavy for a daily merging process. Like @ejgallego said, we are already at the limit with the current process that asks all concerned maintainers for approval. Please don't make it even heavier.\r\n\r\nI'm not trying to make it heavier (see e.g above a proposition). I'm trying to improve the way we interact in the team (and maybe I'm failing too, but then, I'd be happy to have your help to improve my own way of expressing what I have to say). As for making things lighter on other directions than the one I'm talking here, I let you do propositions.\r\n\r\n> You say yourself that there was no problem here, so why exactly are you complaining?\r\n\r\nI'm not complaining on the PR, which again, I find relevant. I'm trying to find a model on which we all agree, and this was the first PR to be committed along the new scheme, so the first PR to discuss about the process and about how to implement the expression \"discussion converge\" which I proposed and which you agreed.\r\n\r\n> I have a strange feeling that this has been said many times already. Could we move on and invest our energy in more productive ways?\r\n\r\nNoone is asking you to put your energy in this issue if you don't want to. As far as I'm concerned, I don't think that a good solution has been given yet and I try to find one. Is the kind of courtesy I'm asking for really supernatural?\r\n\r\nFrom @Zimmi48:\r\n> But honestly, I feel that you should first give a few days or a few weeks so that we see how the process is going and we can judge better whether the amendment is a good idea.\r\n\r\nWe all know that giving space and time for interaction is important, there were enough situations in the team where it mattered, and we can easily observe that it matters in all kinds of social interaction, not only in the team. We can spend time about whether there was enough space for potential discussions in #7023 or not, but this is not my point. The past has shown, in particular wrt my own PRs, that thinking that everything seems in order from one's point of view does not mean that everything is in order for everyone, and we have to take this into account. I would not like to go the other way round myself, as I believe that this would be a pity for the team that, on the name of agility, I start again to commit things, even bug fixes, without enquiring about the opinion of others."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/375361429","html_url":"https://github.com/coq/coq/issues/7042#issuecomment-375361429","issue_url":"https://api.github.com/repos/coq/coq/issues/7042","id":375361429,"user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"created_at":"2018-03-22T16:04:54Z","updated_at":"2018-03-22T16:04:54Z","author_association":"MEMBER","body":"> This morning, I don't know if it should be considered a trivial bug fix or not but I reviewed #7016.\r\n\r\nUmm, IMVVHO this is distant from a \"trivial bug fix\". I'd classify it as \"quite tricky stuff\".\r\n\r\nBut I think you make a good point, but on the other hand I get the feeling that you may be overthinking the process a bit. Maybe I have an easier time as I assume there will never be a perfect process so errors will be made, so I am more interested in fact to increase the tolerance/recovery for errors than in preventing them.\r\n\r\n> About dispatching the work and trusting each other, it seems that I'm one who is spontaneously trusting the most easily, or, at least, I received comments telling that I was trusting too much.\r\n\r\nSure, there is a delicate balance in reviews, but here it is a personal criteria. I was also criticized by approving PRs such as #873 , but I found that criticism quite misguided, I had a look to it, computed my tradeoff, and said \"it looks OK to me\". There was problem? Fine, but not a big deal, the problem is either fixed or the change is rolled back. \r\n\r\n> But ok, let's go in the direction of giving priority to fast merging and to consider that dispatching responsibilities is more important than ensuring a collective discussion.\r\n\r\nI think nobody is proposing to \"give priority to fast merging\", but more on the lines of \"fast merging should be possible\".\r\n\r\nNote the difference between the two statements. I agree with the spirit of your proposal \"every PRs should receive the **right** amount of discussion\", however I am not so sure:\r\n- we have a problem here in the first place: it seems to me that the large majority of PRs are receiving a fair amount of discussion,\r\n- that some kind of \"formal time system\" is the right tool for that. I'd rather trust the person in charge of the subsystem to determine when the amount of required discussion has been reached.\r\n\r\n> Now, **how do you implement the case of a disagreement after a merge**. ...\r\n\r\nI guess that's fairly easy, you would just open an issue or add a comment in the PR expressing your concerns. Whether a patch has been merged or not doesn't seem very relevant to me in this context."}}
{"actor":{"display_login":"ejgallego"}}