how to run linter

Stream: lean4

[Asei Inoue]

I would like to know how to use the docBlameThm linter.
It does not seem to be possible to enable it with set_option.

[Johan Commelin]

Add #lint to the bottom of your file.

[Johan Commelin]

You might need a suitable import. Do you want to run it on a file in a branch of mathlib, or in some other project?

[Asei Inoue]

in other project

[Asei Inoue]

How can I enable the linter for the whole project instead of on a file-by-file basis?

[Kim Morrison]

Look for how Mathlib or Batteries CI invokes runLinter.

[Asei Inoue]

@Kim Morrison
Thanks.
but why option version is missing? docBlameThm is useful linter...

[Asei Inoue]

Why is there both a linter executed via the #lint command and a linter executed via set_option in the first place...?

[Asei Inoue]

I would always find it more convenient for the linter to be able to switch between run/stop with set_option, is there a reason for this?

[Kim Morrison]

There are two completely independent sets of linters, environment linters controlled by #lint and runLinter, and syntax linters controlled by set_option. They have nothing to do with each other except the name.