-
Notifications
You must be signed in to change notification settings - Fork 696
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Import hygiene and miscellaneous fixes. #3537
Conversation
Signed-off-by: Edward Z. Yang <[email protected]>
@ezyang Are there reasons
E.g. #3476 the #3476 (comment) comment is not addressed. Please, if you rush commit in, address obvious issues yourself. I don't think there is written process, but IMHO it worked quite well when @23Skidoo works as a gatekeeper, i.e. merges stuff (thanks for that!) Apart from that, this PR LGTM. |
Let me say a little more about rushing. There is an inherent tension in all software projects between stability and forward progress. And so the question I would ask you is this: should Cabal value stability or forward progress more? If we value forward progress, we need to also value refactoring. And the reality of refactoring is that these are large, non-local changes, which take disproportionately more time to code review, and are most harmed by a long lead-time into Cabal. Take #3525. Not only is this going to take a lot of time to review, I'm pretty sure that it conflicts with a refactor that @dcoutts is working on to fix exception handling in new-build. So it is really harmful to keep refactor PRs in the queue for too long. We really do need to rush! |
This is precisely why we use Github merge: Travis the CI verifies that we don't have something which breaks the build in the commit / branch you push / merge. It's not perfect, but still better than (even rare) accidental breakages. I'm also quite sure that people are lazy to verify with every GHC we tend to support, that boring job is left for CI on purpose. |
(FYI: I edited my above comment, in case you didn't see.) |
I agree with @ezyang's points and appreciate his efforts. In general, I think we should move in the direction of less bureaucracy, which among other things means trusting developers with a commit bit to merge open PRs (after all, that's what the commit bit is for). I also think that non-GitHub merges are fine, since our build bots will catch any eventual errors anyway, in which case the offending commits can be reverted. |
Merged, thanks! |
This is a hard question. I do value forward progress, do value your efforts, and I have bitten myself by long-lead time and numerous rebasing due conflicts (not in To return to #3525. I do agree that it's welcomed change. But I'm a bit confused. There is an issue to introduce About large refactorings. I have no silver-bullet for this. Try to split them into smaller PRs (as you did with I do dislike that we step over CI, and push to If I can propose a rule: let someone else than the author merge the PR. |
Signed-off-by: Edward Z. Yang [email protected]