-
Notifications
You must be signed in to change notification settings - Fork 704
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
Don't send non-existent extra-lib-dirs to ghc #8510
Conversation
@gbaz: is this ready for review? |
Sure! |
Hey, why is there no label, in that case? :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems safe (famous last words). Is there a cheap way of protecting this PR from accidental reversion via a test?
Should |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I wonder about the placement in Distribution.Simple.GHC
. Is this something GHC specific or shouldn't these non-existing directories be filtered out earlier in the pipeline, like after parsing?
Also, I agree with @Ericson2314 's concern that non-existing include directories should also be filtered out.
There is no place to filter these things out earlier in the pipeline uniformly afaik, because the parsing phases are pure. We only hit IO on ghc invocation. I looked into doing it for includes, but the place includes are set to send to ghc is elsewhere in the pipeline, and so i think it would be a rather invasive and fragile change compared to this, and also one with no particular purpose other than symmetry. So I'd rather not. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fine with me.
@Mikolaj : I can't remember whether the policy was to (a) squash the commit with the changelog into one commit with the feature or (b) to keep it separate. Lines 240 to 242 in 7babda9
|
I think it may be recommending it only because squashing requires one more mental action and |
Ultimately it's up to the user and, normally, the users sets the label. |
Doh, not user, but dev, PR author. |
You could add something like this to |
I'd like to keep CONTRIBUTING.md short and not (too much) opinionated. Perhaps just reduce the nudge? Or focus it on the most obvious case? "If your pull request consists of several fix-up commits (not every commit compiles or they just don't help in understanding the PR, e.g., by separating formatting, refactoring and real functionality changes), please use |
I think we should lean to squashing unless the different commits are really different changes. (a) it makes for a clearer history (I doubt anyone benefits from tens or hundreds of commits "add changelog"), (b) individual commits are not tested by the ci, only the overall PR is, isn't it? in that case, there may be unbuildable "middle" commits that will severely complicate any future |
Right, different trade-offs and tastes. Given that the PR page retains the original commits, I'd not worry about separating formatting, refactoring and (multiple) changes. However, we may want to migrate off github in the future and I'm can't be sure the PR commits are going to be migrated as well (given that the feature branches is deleted). Perhaps let's leave it as is. :) |
Filters extra-lib-dirs before passing to GHC. Resolves #6492