apply mathlib linters?

Stream: FLT

[Kevin Buzzard]

This is a hopefully easy CI question. I get PRs which pass CI but which have e.g. over 100 character lines, or definitions without docstrings etc. Is it easy just to get mathlib linters running on FLT with some easy addition to the toml? Now we've switched to a toml I can't just apply the old algorithm of "cut and paste from lakefile.lean".

[Edward van de Meent]

now you can "cut and paste from Carleson's lakefile.toml" (found here)

[Edward van de Meent]

of course this will be up for customisation, as i don't think that has all of mathlibs linters enabled either, but it should help get started with the syntax

[Edward van de Meent]

let me try and find all linters mathlib has enabled by default...

[Edward van de Meent]

Here is (as far as i can tell) the toml equivalent of mathlibs options

[leanoptions]
weak.linter.docPrime = false
weak.linter.hashCommand = true
weak.linter.oldObtain = true
weak.linter.refine = true
weak.linter.style.cdot = true
weak.linter.style.dollarSyntax = true
weak.linter.style.header = true
weak.linter.style.lambdaSyntax = true
weak.linter.style.longLine = true
weak.linter.style.longFile = 1500
weak.linter.style.missingEnd = true
weak.linter.style.multiGoal = true
weak.linter.style.setOption = true
pp.unicode.fun = true
autoImplicit = false

[moreserveroptions]
linter.docPrime = false
linter.hashCommand = true
linter.oldObtain = true
linter.refine = true
linter.style.cdot = true
linter.style.dollarSyntax = true
linter.style.header = true
linter.style.lambdaSyntax = true
linter.style.longLine = true
linter.style.longFile = 1500
linter.style.missingEnd = true
linter.style.multiGoal = true
linter.style.setOption = true

[Edward van de Meent]

(hope this helps)

[Kevin Buzzard]

This definitely helps! I have this vague idea that there are two kinds of linters -- syntax linters and some other kind -- does this explain why there are two lists?

[Kevin Buzzard]

Oh no that can't be it because the lists are extremely similar!

[Damiano Testa]

No, these are all syntax linters. The two lists should be the default in lake build (with weak) and the default value for when you open a file (without weak).

[Damiano Testa]

I think that mathlib makes no distinction: all linters that are active in CI are also active on VSCode and vice versa.

[Damiano Testa]

The "other" linters, namely the environment linters, are run by writing #lint in your file and they check everything in the environment so far (that is, from where you write it and up). For making them active in CI, Mathlib uses a step which runs env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib.

[Damiano Testa]

For instance, the simpNF linter is activated in that step.

[Kevin Buzzard]

Yeah Iinted a PR today and the simpNF linter failed and that was what actually pushed me to ask the question