Mathlib linters in cslib

Stream: computer science

[Fabrizio Montesi]

Does anybody know how we can activate the linters used in mathlib using the lakefile toml format?

[Damiano Testa]

Under [leanOptions], adding

weak.linter.mathlibStandardSet = true

should activate all the ones that are active in mathlib.

[Bhavik Mehta]

What does the weak. prefix do here? I've been using linter.mathlibStandardSet = true instead

[Damiano Testa]

I'm not sure: what happens if you do not import the file with the standardSet option?

[Eric Wieser]

weak means that if the setting doesn't exist you don't get an error

[Eric Wieser]

e.g. if you forgot to import mathlib in a file

[Bhavik Mehta]

Ah! I was wondering why that happened, although I deliberately didn't import mathlib last time it happened ;)