-
Notifications
You must be signed in to change notification settings - Fork 80
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
Remove trailing whitespace #773
Remove trailing whitespace #773
Conversation
I agree that trailing whitespaces have no place in the development. |
What's the process for getting this merged? |
I personally don't mind, but this is a commit that might induce a lot of pain (as in conflict) if other developers have unmerged content. @mattam82 @yforster @MevenBertrand would you happen to know? |
According to the docs, it shouldn't be hard to rebase on top of a whitespace-only change. The following procedure should work (I haven't tested though):
|
My biggest worry here would be that we get lots of clashes with the work on SProp by @yannl35133. I have unmerged stuff, but its mostly self-contained. @kyoDralliam also has new things, but I think as of now also mostly self-contained. |
Is this #708? It has a bunch of merge conflicts with coq-8.16 (even with coq-8.14), but I've tested the above strategy by finding the git rebase ${WHITE_SPACE_SHA}^
git rebase -Xignore-space-at-eol ${WHITE_SPACE_SHA}
git diff --name-only --diff-filter=U | xargs git rm && GIT_EDITOR=true git rebase --continue The third line is needed because there was one commit that deleted a file with a whitespace change, which So this strategy seems to work fine |
I'm fine with removing whitespace. I think @yannl35133 actually wanted that as well, IIRC. |
We could also imagine having a linter for this. But the best is simply for everyone to use an editor that does not introduce them in the first place? |
Can we have a vscode option in the workspace file that's in the repo anyways? |
We could, but it's also on by default no? |
I think
is the default |
Then I'm all for changing it in the repo. |
I confirmed this by running "Preferences: Open default settings (JSON)" |
Rebasing SProp to Coq 8.16 is going to be non-trivial in any case, so I'm fine with dealing with this when I'll do it. |
With ``` git grep --name-only ' $' '*.v' | xargs sed -i 's/\s\+$//g' ```
e43b9d4
to
e448965
Compare
https://github.com/MetaCoq/metacoq/actions/runs/3516675088/jobs/5894539090 seems to have been running for half an hour already after completing the "Complete Job" step... |
CI passed, this is ready for merge |
With
(Not sure if you want this sort of PR, but it makes development a bit easier for me because my editor autoremoves trailing whitespace)