False positive on `←` style linter

Stream: mathlib4

[Thomas Murrills]

Currently the lack of space before the backtick in "\`←\`"is activating the style linter: https://github.com/leanprover-community/mathlib4/pull/10991#discussion_r1503341170

[Eric Wieser]

(in `←` , you mean?)

[Thomas Murrills]

Yes! I'm not quite sure why Zulip allows backslashes to escape backticks, but doesn't remove the backslashes... :sweat_smile:

[Thomas Murrills]

Oh, I think I can fix this.

[Thomas Murrills]

When exactly is annotate_comments in lint-style.py meant to annotate a line as being in a comment? After all, part of a line can be a comment (def x := by -- note), and this isn't currently captured; but if any part of the line involves /- (and it does not include -/), we consider the line to be in a comment. Is the heuristic "the line should considered to be in a comment iff the whole line is in a comment"?

The issue with this specific example is that we have /- ... -/ in a code block in above, and the presence of -/ sets in_comment to False, leading to the rest of the comment not being considered in_comment (given the current logic).

[Thomas Murrills]

#10994 attempts to improve the heuristics a bit and handle nested comments more reliably, without introducing character-by-character parsing. I'd like to test it a bit, though. We don't have tests for linters, right? Or do we?