Zulip Chat Archive

Stream: general

Topic: line length


Patrick Massot (Aug 13 2021 at 12:21):

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

Anne Baanen (Aug 13 2021 at 12:24):

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

Patrick Massot (Aug 13 2021 at 12:31):

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

Patrick Massot (Aug 16 2021 at 07:58):

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 (Aug 16 2021 at 08:10):

Copied, thank you.

Julian Berman (Aug 16 2021 at 09:32):

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)


Last updated: Dec 20 2023 at 11:08 UTC