github diffs trick

Stream: mathlib4

[Kevin Buzzard]

issue2.png
issue1.png

This sort of thing is happening when I make mathlib4 PRs because when I edit mathlib4 files VS Code isn't clearing up after me, removing spaces at the end of lines and adding a newline at the end of a file, right? I also think that this doesn't happen when I edit mathlib3 files, because someone added a clever tweak to a config file. Am I talking nonsense or is there a trick we're currently missing?

[Ruben Van de Velde]

This looks like your editor is fixing bad whitespace in mathlib4, which I guess it didn't do in 3

[Kevin Buzzard]

Yes, but my editor also added those bad whitespaces! I suspect I fixed them manually, possibly by accident.

[Scott Morrison]

I added the .vscode directory to the mathlib4 repository a while back. It tells VSCode to normalize whitespace, exactly according to the conventions mathlib uses. I suspect what happened is that commits before I added this had random whitespace, and you're now seeing things slowly come back to match the conventions.

[Scott Morrison]

If this is annoying, we could open and resave every file in VScode, I guess.

[Kevin Buzzard]

I see! So the problem will go away on its own now then. Thanks!

[Daniel Fabian]

you might also want to disable whitespace changes:

image.png

[Julian Berman]

Also pre-commit (https://pre-commit.com/hooks.html) is quite nice. It can catch or autofix (either locally or in CI) these and other kinds of things. (E.g. rather than manually opening and closing vscode, running pre-commit run --all-files with a pre-commit config that prevented trailing whitespace will go and fix all the files in the repo).

[Patrick Stevens]

Note that you can append ?w=1 to a pull request URL in GitHub to see the diff without whitespace changes, e.g. https://github.com/leanprover-community/mathlib/pull/7701/files?w=1 (not that that PR actually contains any whitespace changes)

[Patrick Stevens]

(same as the UI option just above, but easier to type)