linters repeat error messages

Stream: lean4

[Floris van Doorn]

Minor issue, but linters repeat some error messages. E.g.

import Mathlib.Tactic.Core
set_option foo true in
example : True := trivial

outputs

Test.lean:2:0
unknown option 'foo'
Test.lean:2:0
linter Lean.Linter.MissingDocs.missingDocs failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.header.headerLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.DocPrime.docPrimeLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.globalAttributeInLinter.globalAttributeIn failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.HashCommandLinter.hashCommandLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.DupNamespaceLinter.dupNamespace failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.multiGoal.multiGoalLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.oldObtainLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.refineLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.UnusedTactic.unusedTacticLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.longFile.longFileLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.setOption.setOptionLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.longLine.longLineLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.cdotLinter failed: unknown option 'foo'
Test.lean:2:0
linter Mathlib.Linter.Style.missingEnd.missingEndLinter failed: unknown option 'foo'

[Sebastian Ullrich]

If it's just Mathlib linters, this should probably be moved to #mathlib4?

[Floris van Doorn]

I think it's the linter framework.

import Lean
set_option foo true in
example : True := trivial

gives

Test.lean:2:0
unknown option 'foo'
Test.lean:2:0
linter Lean.Linter.MissingDocs.missingDocs failed: unknown option 'foo'

[Sebastian Ullrich]

Ah, I missed that one. Could you file an issue?

[Eric Wieser]

I think this is because the linters re-run the set_option commands so that they can read the modified options

[Floris van Doorn]

lean#7148