<div dir="ltr">Hi Joachim,<br><br><div><div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> * Merging unapproved, but implemented proposals.<br>
<br>
This would mean that there would be some proposals in the directory<br>
<a href="https://github.com/ghc-proposals/ghc-proposals/tree/master/proposals" rel="noreferrer" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals/tree/<wbr>master/proposals</a><br>
<br>
that were not vetted, discussed and approved. Is that desirable? It<br>
seems it would water down the status of the rest.<br></blockquote><div><br></div><div>I would consider that they were implicitly vetted by whomever merged the CR into GHC master. Or is it too much of a stretch? Obviously they are changes which have somewhat side-stepped the process which probably only happens because the dust hasn't quite settled yet.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
About documentation: The proposal can still be linked, during its<br>
implementation. Are you worried that the pull request will be lost<br>
somehow?<br></blockquote><div><br></div><div>Not really. But if a proposal is not vetted, referring to it is less strong an argument when you ask for merge, of course. Merge serves as a witness of vetting. On the other hand, if this was the only reason to merge proposal, we should remove them when they are implemented. What I was trying to get at, is that we probably want proposals to stay, because they serve as documentation even after they have been implemented.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
You also write that the manual should link proposals (I guess that<br>
applies to all proposals). I don’t think we would be doing our users<br>
a favor here; they expect and deserve a comprehensive and self-<br>
contained manual.<br></blockquote><div><br></div><div>To be fair, I said "could".<br><br></div><div>And the idea is that a proposal contains a lot beyond what the manual will. The entire specification section must make it to the manual. However, the motivations will usually be much shortened, and the alternatives will typically not be in a manual at all. A proposal also has a link to the github discussion which can give really insightful historical perspectives on a feature. So giving a link to the proposal could help someone who, for instance, is considering contributing an extension to a given feature. It's not something that should be prominent. But can feature in a "further reading" section, together with the relevant scientific articles.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
We briefly had this discussion a while ago. The rationale to not<br>
close tickets that were not officially rejected is because<br>
contributor motivation is a scarce resource, and me just going<br>
around closing people’s proposals just because they are not able to<br>
press forward a lot.<br>
<br>
I am nudging stagnant proposals, and eventually mark them as<br>
“dormant”, as a more friendly way of closing them. Many authors<br>
then close them voluntarily when they have abandoned it.<br>
<br>
Note that the overview at<br>
<a href="https://github.com/ghc-proposals/ghc-proposals" rel="noreferrer" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals</a><br>
links to “≡ List of proposals under discussion”<br>
which includes only the somewhat active propsoals.<br>
<br>
Maybe I can close dormant porposals when nothing has happened in<br>
$n$ months, with a friendly message that it can be re-opend any<br>
time.<br></blockquote><div><div><br></div><div>I agree that it is a matter of reading people's psychology right. No mean feat!<br><br></div><div>I would personally go for closing after a while. Certainly with the friendly message!<br></div></div></div><br></div></div></div></div>