whitespace in emacs

Stream: general

[Adam Topaz]

I have found that some lines in my lean files end up with trailing whitespace, after editing them in emacs. This is probably always my fault for adding spaces and not deleting them.

It seems that vscode has some automatic magic that gets rid of these trailing spaces. So if I commit some files with emacs, then make some edits in vscode and commit from vscode, I get a lot of small whitespace only diffs, that I would like to avoid.

Does anyone know of some linter for emacs that gets rid of trailing unnecessary whitespace?

[Reid Barton]

This isn't exactly what you asked for (and I'm curious too) but global-whitespace-mode will make it pretty obvious if you leave trailing whitespace (or other whitespace infelicities such as tab characters) in your file. I recommend turning off everything related to the display of ordinary spaces and newlines.

[Simon Hudon]

I have this line in my init.el file:

(add-hook 'before-save-hook 'delete-trailing-whitespace)

[Simon Hudon]

Instead of highlighting the trailing spaces, it just deletes them every time I save.

[Adam Topaz]

Thanks! delete-trailing-whitespace works exactly as I expected!

[Julian Berman]

also also not what you asked for, but pre-commit (https://pre-commit.com/) is very useful, and the trailing-whitespace hook if you configure it will complain at you if you try to commit files with trailing whitespace

[Adam Topaz]

Does pre-commit work with magit?

[Simon Hudon]

I haven't had trouble with the two

[Adam Topaz]

Great! Maybe I'll be able to uninstall vscode soon :eyes:

[Simon Hudon]

Btw, have you tried VS code with Coq? I hear it's pretty good

[Adam Topaz]

No I havent

[Adam Topaz]

I only played with Coq a little bit, using proof general and coqide

[Simon Hudon]

Me too. Actually, I started appreciating Coq much more once I tried Proof General. But I hear Proof General is the only one that can't do parallel proof compilation