Zulip Chat Archive

Stream: general

Topic: Style linters

Yaël Dillies (Oct 10 2021 at 20:19):

Quick question so that I aboid writing wrong stuff. Are the style linters written in Lean or in Python?

Julian Berman (Oct 10 2021 at 20:31):

There's one (or multiple) in each I think -- the #lint command is written in lean, the mathlib style linter is in Python

Julian Berman (Oct 10 2021 at 20:32):

Style linter is here: https://github.com/leanprover-community/mathlib/blob/master/scripts/lint-style.py

Julian Berman (Oct 10 2021 at 20:33):

Lean linter is here: https://github.com/leanprover-community/mathlib/blob/0b8a858f92391d196faac613528aa8d19f382998/src/tactic/lint/frontend.lean (or at least the entry point)

Yaël Dillies (Oct 10 2021 at 20:39):

I meant the style linters. I know it would be hell to write the code linters in anything else than Lean :smile:

Last updated: Dec 20 2023 at 11:08 UTC