linting a project

Stream: general

[Kevin Buzzard]

I just got a lean project (the real number game) compiling with current mathlib. How do I now run the linter on it? I have this feeling that linting my own files might teach me to write more hygenic code in general; I have no formal training as a programmer and still have a lot to learn.

[Kevin Buzzard]

Oh is there just some command line thing I can type which lints a project?

[Kevin Buzzard]

I'm completely new to linting, I didn't even know #lint was a thing until a few weeks ago

[Mario Carneiro]

The usual use is to put #lint at the bottom of your file

[Mario Carneiro]

I think there is also a way to use it project wide, that is used in CI

[Gabriel Ebner]

The CI integration is very much handtailored tot mathlib at the moment.

[Mario Carneiro]

is mk_all.sh also mathlib tailored?

[Gabriel Ebner]

Not really.

[Mario Carneiro]

but if you #lint a file with only import all, you only get global lints, right?

[Kevin Buzzard]

My project is here https://github.com/ImperialCollegeLondon/real-number-game , it's only very small, I'd just like to lint all of it and probably faced with a huge pile of errors. I thought it might be instructive to fix them

[Gabriel Ebner]

#lint will only lint the current file, #lint_all will lint everything including core and mathlib. The code is reasonably modular, you van check what #lint_mathlib does.