add linter for whitespace checking

[katrinafyi]

This adds scripts/lint.sh to check and apply trailing whitespace trimming. This should prevent cluttering diffs with whitespace changes in future.

It can be used as lint.sh to check and lint.sh fix to apply replacements in-place.

Given the amount of pending work, it is probably a bad time to merge this PR now. It would also be good to integrate the checks with dune and/or CI checks.

Edit: The script is now lint.py and it accepts a list of files/dirs as arguments.

[katrinafyi]

Maybe instead of a bespoke grep/sed solution, we can use Git's whitespace handling. For example, to check whitespace,

git diff-tree --check 4b825dc642cb6eb9a060e54bf8d69288fbee4904 HEAD -- ':!mra_tools' 

which excludes mra_tools and uses the magic git hash for the empty directory to check all indexed files.

However, this can vary in behaviour if core.whitespace is set locally. It is also difficult to apply changes via git (https://stackoverflow.com/a/15398512) so sed may still be needed.

[katrinafyi]

I have ported the script to Python (it was inevitable) and removed the commit which applied whitespace fixes.

This makes the PR easier to merge and we can all run the linter on our own code without merge conflicts.