Bug in commandStart linter error message

Stream: mathlib4

[Michael Rothgang]

I found an example where the commandStart linter's error is misleading: in the following example, the error should be "remove a space", but it's "remove a line break".

import Mathlib.Init

set_option linter.style.commandStart true

-- note: space after the "in "; the diagnostics are a bit misleading

/--
warning: remove line break in the source

This part of the code
  'in ⏎
-- TODO:'
should be written as
  'in
-- TODO:'

note: this linter can be disabled with `set_option linter.style.commandStart false`
-/
#guard_msgs in
open scoped Classical in
-- TODO: add longer docs!
-- extendLocally: takes trivialisation e as parameter, and a basis b of F
variable {V F} (b e) in
def foo : Nat := 1

/--
warning: remove line break in the source

This part of the code
  'in ⏎
def'
should be written as
  'in
def bar'

note: this linter can be disabled with `set_option linter.style.commandStart false`
-/
#guard_msgs in
open scoped Classical in
def bar : Nat := 1

[Michael Rothgang]

CC @Damiano Testa

[Damiano Testa]

It is true that this is misleading, but it also seems true that removing the line break could be what is wanted here, right?

[Damiano Testa]

That is, the code below should also be allowed, I think:

open scoped Classical in -- TODO: remove this
variable {V F} (b e) in
def foo : Nat := 1

[Michael Rothgang]

In this particular case (open Classical in) I would say it's not wanted. This might be different for other syntax.

[Damiano Testa]

So, I would leave this as "the linter suggests a valid way of complying, there may be other ways that are also compliant and may be better on a case-by-case basis".

[Damiano Testa]

Does this seem like a reasonable summary?