line length

Stream: general

[Patrick Massot]

Does anyone has a git hook that checks mathlib line lengths before pushing?

[Anne Baanen]

I think you can just call ./scripts/lint-style.sh from the pre-push hook?

[Patrick Massot]

Yes, this is the general idea but I was asking whether someone already figured out the details.

[Patrick Massot]

For the record, I ended up writing

#!/bin/sh

./scripts/lint-style.sh

in mathlib/.git/hooks/pre-push and it does the job.

[Scott Morrison]

Copied, thank you.

[Julian Berman]

If it's useful as an alternative, in neovim I hooked up https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending#mathlib-style-linting to show them inline (i.e. as normal diagnostics) while editing a file in mathlib -- that's probably doable equally easily in VSCode (if that's useful I can try to look up specifically how to do so)