Remove trailing whitespace

[JasonGross]

With

git grep --name-only ' $' '*.v' | xargs sed -i 's/\s\+$//g'

(Not sure if you want this sort of PR, but it makes development a bit easier for me because my editor autoremoves trailing whitespace)

[TheoWinterhalter]

I agree that trailing whitespaces have no place in the development.

[JasonGross]

What's the process for getting this merged?

[TheoWinterhalter]

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?

[JasonGross]

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):

1. git rebase ${WHITE_SPACE_SHA}^, resolve any conflicts --- this will bring the branch up to date with the commit right before the whitespace change
2. git rebase -Xignore-space-at-eol ${WHITE_SPACE_SHA} --- this should (hopefully) rebase atop the whitespace change without conflicts
3. (optional) git rebase --whitespace=fix ${WHITE_SPACE_SHA} --- this should (hopefully) strip any newly introduced trailing whitespace
4. git rebase coq-8.16 (or whatever branch)

[yforster]

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.

[JasonGross]

My biggest worry here would be that we get lots of clashes with the work on SProp by @yannl35133.

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 merge-base upstream/coq-8.14 upstream/sprop (giving afb2b5a), adding a commit on top of that with git grep --name-only ' $' '*.v' | xargs sed -i 's/\s\+$//g' && git commit -am "Remove whitespace" && export WHITE_SPACE_SHA="$(git rev-parse HEAD)", and then doing

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 -Xignore-space-at-eol doesn't handle as per https://stackoverflow.com/a/54232519/377022

So this strategy seems to work fine

[yforster]

Let's wait for #783 and #781, then we can fix the conflicts here and merge

[mattam82]

I'm fine with removing whitespace. I think @yannl35133 actually wanted that as well, IIRC.

[TheoWinterhalter]

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?

[yforster]

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?

[TheoWinterhalter]

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?

[yforster]

I think

"files.trimTrailingWhitespace": false

is the default

[TheoWinterhalter]

Then I'm all for changing it in the repo.

[yforster]

I confirmed this by running "Preferences: Open default settings (JSON)"

[yannl35133]

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.

[JasonGross]

Let's wait for #783 and #781, then we can fix the conflicts here and merge

I've fixed the conflicts, this should be ready for merge

[JasonGross]

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...

[JasonGross]

CI passed, this is ready for merge