chore: enable lint in CI

[kim-em]

After cleaning up some unused arguments in #154, this proposes that all remaining linting problems go in nolints.json, and we enable the linter in CI.

[JLimperg]

Is there a way to disable certain linters? I'm in favour of enabling linting, but I don't plan to systematically document Aesop, so I wouldn't want to fight the docBlame linter all the time.

[kim-em]

Hmm, as far as I'm aware there isn't a way to turn off environment linters via runLinter.

@digama0 or @adomani, any ideas for how we could let people turn off e.g. docBlame easily from a lakefile? We either need more command line arguments for runLinter, or have the environment linter framework pay attention to a package level option?

[josojo]

Others have done it like this: https://plmlab.math.cnrs.fr/nuccio/mathlib4/-/blob/splittingfieldch/Mathlib/Data/FP/Basic.lean?ref_type=heads#L164

not sure whether this is good enough...

[kim-em]

Others have done it like this: https://plmlab.math.cnrs.fr/nuccio/mathlib4/-/blob/splittingfieldch/Mathlib/Data/FP/Basic.lean?ref_type=heads#L164

not sure whether this is good enough...

These are syntax linters, rather than environment linters.