error lens in lean4

Stream: general

[Asei Inoue]

error lens (https://marketplace.visualstudio.com/items?itemName=usernamehw.errorlens) is very popular extension in lean community.
I think it would be better lean4 extension have the feature similar to error lens.

[Asei Inoue]

instead, it would be good to have extension pack

[Marc Huisinga]

The default functionality of ErrorLens is quite visually noisy and asking some users on their opinion about it revealed that quite a few people would prefer not to have it enabled by default (e.g. because highlighting the entire line and displaying text after it is noisy, because squishing Lean's multi-line errors into one line often isn't helpful and displaying them on multiple lines next to the text is even noisier, etc.). This is ultimately one of the reasons why we implemented vscode-lean4#585 as a less visually noisy alternative catered to Lean.
If the functionality that is provided by ErrorLens and not by our extension can't be enabled by default, I don't see much of a strong reason to duplicate it into the Lean VS Code extension.

[Asei Inoue]

@Marc Huisinga Thank you!!

[Snir Broshi]

Marc Huisinga said:

The default functionality of ErrorLens is quite visually noisy and asking some users on their opinion about it revealed that quite a few people would prefer not to have it enabled by default (e.g. because highlighting the entire line and displaying text after it is noisy, because squishing Lean's multi-line errors into one line often isn't helpful and displaying them on multiple lines next to the text is even noisier, etc.). This is ultimately one of the reasons why we implemented vscode-lean4#585 as a less visually noisy alternative catered to Lean.
If the functionality that is provided by ErrorLens and not by our extension can't be enabled by default, I don't see much of a strong reason to duplicate it into the Lean VS Code extension.

I use Error Lens with Lean. I love the gutter decorations, but I think if anything then the Lean extension is even visually noisier than Error Lens with its yellow squiggles which appear for almost anything.
Is there a way to turn off all yellow squiggles? (but not the red ones)
Specifically these are very visually noisy:

• declaration uses 'sorry'
• This line exceeds the 100 character limit, please shorten it!
• automatically included section variable(s) unused in theorem

[Asei Inoue]

@Snir Broshi You’re talking about how to silence specific linter?

[Snir Broshi]

No I want the lint, I just hate the visual noise

[Aaron Liu]

for VSCode, there's a hard cap of 500 squiggles, so if you put 500 overlapping squiggles in one place it won't generate any more beyond that

[Snir Broshi]

That would also eliminate red squiggles, which will make it hard to spot the error.
The errors I mentioned above aren't about a specific position in the line, so a gutter icon on the line should be enough.

[Yaël Dillies]

Snir Broshi said:

This line exceeds the 100 character limit, please shorten it!

This one is particularly annoying as it gives on the whole line, hiding other potentially useful warnings. Typical case is that I am removing unused lemmas in a simp call, but sometimes I remove a line break and suddenly the line is too long and all the visual info about which lemmas are unused disappears until I add the line-break back... Would it be possible to put the squiggle on the characters past the limit only?

[Snir Broshi]

Or even just on the 101st character

[Damiano Testa]

Ah, localising the error on a subset of the line is easy.

[Damiano Testa]

Just the 101st character seems too minimal, but the interval starting at 101 would seem reasonable to me.

[Marc Huisinga]

Snir Broshi said:

but I think if anything then the Lean extension is even visually noisier than Error Lens with its yellow squiggles which appear for almost anything.

Just to be clear: the squigglies are a default functionality of VS Code, not the Lean extension. It's one of the ways in which VS Code renders warnings provided by the extension (or rather, the language server and the elaboration code it runs, which is extensible by meta code).
By default, the Error Lens extension will also mark every single line that has a yellow squiggly with a yellow background color and text describing the warning next to it. If your editor feels noisy with squigglies, surely it will feel even more noisy with yellow background coloring for the whole line and warning text at the end of every line, no matter how small the squiggly in that line was?

Snir Broshi said:

Is there a way to turn off all yellow squiggles? (but not the red ones)

I don't think that this is a good idea in general. When there is a warning on a line, the presence of which you are made aware of by some part of the UI, then the editor should also display the specific location of that warning within the line, otherwise it is very easy to be confused for most warnings (e.g. consider a line with multiple similarly-named parameter declarations where one of them generates an unused variable warning).

That said, I agree that for some specific linter warnings (like the line character limit linter of Mathlib), it might be desirable to display them everywhere but as a squiggly (i.e. to display them in VS Code's 'Problems' view, to have them interact correctly with the 'Go to Next Problem' command, to have them show up in the InfoView and in the gutter, etc.), but this isn't supported by VS Code because the diagnostic API inherently ties the squigglies to lots of other functionalities with no configurable middle-ground on a per-diagnostic (or even just per-diagnostic code) basis.

If you really want to disable all warning squigglies, then to my knowledge the only way to do so is to modify your color theme and make them transparent by adding

"workbench.colorCustomizations": {
  "editorWarning.foreground": "#00000000"
}

to your settings.json in VS Code ('File' > 'Preferences' > 'Settings' > 'Open Settings (JSON)' button in the top right).

Snir Broshi said:

• This line exceeds the 100 character limit, please shorten it!

This warning is generated by the style linter in Mathlib, not core.

[Snir Broshi]

Marc Huisinga said:

It's one of the ways in which VS Code renders warnings provided by the extension (or rather, the language server and the elaboration code it runs, which is extensible by meta code).

Yes I'm aware, which means that they'll disappear if Lean chooses not to report them. I understand that some people use the "problems" feature, but I'd like some warnings to be gutter-only.

If your editor feels noisy with squigglies, surely it will feel even more noisy with yellow background coloring for the whole line and warning text at the end of every line, no matter how small the squiggly in that line was?

Not for me, personally the background color is way cleaner than squigglies. I've disabled the text for these specific errors in ErrorLens's settings.

When there is a warning on a line, the presence of which you are made aware of by some part of the UI, then the editor should also display the specific location of that warning within the line, otherwise it is very easy to be confused for most warnings (e.g. consider a line with multiple similarly-named parameter declarations where one of them generates an unused variable warning).

I only mentioned warnings which were about the whole line/declaration.

this isn't supported by VS Code because the diagnostic API inherently ties the squigglies to lots of other functionalities with no configurable middle-ground

Sure but I don't want them to be reported as problems at all, so VSCode is not the blocker here

If you really want to disable all warning squigglies

I don't, but it may be worth sacrificing useful squigglies to hide the spammy ones

[Marc Huisinga]

Snir Broshi said:

I understand that some people use the "problems" feature, but I'd like some warnings to be gutter-only.

You will not even be able to read the warning message if the linter warning is only displayed in the gutter, since VS Code unfortunately has no workable mechanism for hovers in gutter decorations. I'm also not convinced that we should have warnings in the gutter that you can't navigate to using VS Code's problem navigation commands. I'd certainly expect to be able to automatically navigate to a warning that VS Code displays to me as such using the usual keyboard shortcuts.

Snir Broshi said:

I only mentioned warnings which were about the whole line/declaration.

The paragraph you are responding to explicitly refers to the question about turning off all yellow squigglies.

[Snir Broshi]

Snir Broshi said:

Specifically these are very visually noisy:

• declaration uses 'sorry'
• This line exceeds the 100 character limit, please shorten it!
• automatically included section variable(s) unused in theorem

Found another example of one that bothers me often: tactic does nothing on #check in a proof

[Kevin Buzzard]

Although these might be visually noisy, all of them other than "declaration uses sorry" are issues which should probably be fixed immediately and are probably easy to fix immediately; in my experience these are not annoying because I just fix them and then they go away.

I have found declaration uses 'sorry' noisy in my work though, not least because I am involved in projects which are full of sorrys, but for those projects I switch off sorry warnings completely with

# Switch off warnings generated by `sorry`
warn.sorry = false

in my lakefile.lean.

[Damiano Testa]

I think that the unused #check had been brought up before as well The linter should probably ignore those, since the #check tactic is noisy anyway, so would not make it past mathlib's CI.

[Kevin Buzzard]

Oh wait I have misunderstood the #check one -- I thought Snir was just complaining about the unused tactic linter in general (and the fix is to delete the unused tactics). What is the issue with #check?

[Damiano Testa]

I think that this is the tactic #check, which indeed is always unused.

[Damiano Testa]

So, you get the output of #check and also a warning from the linter telling you that #check is doing nothing.

[Aaron Liu]

and the warning covers up the useful info of what the #check tactic outputs

[Aaron Liu]

can we make the unused tactic linter not lint on noisy tactics maybe

[Snir Broshi]

Tried Marc's solution to hide all warning squigglies and so far I'm lovin it (though I fear missing an important warning):

---

By default: image.png

---

Error Lens + errorLens.excludeByMessage + Marc's workbench.colorCustomizations: image.png

---

all of them other than "declaration uses sorry" are issues which should probably be fixed immediately and are probably easy to fix immediately; in my experience these are not annoying because I just fix them and then they go away.

I regularly have temporary comments that are over the limit, I'm surprised that it's not common.
Also even when the warnings are only for a minute, such as when adding a parameter to a theorem or a lemma to a simp/grind, I still find these warnings incredibly annoying.

I agree it's usually fine when it comes to automatically included section variable, or tactic does nothing on tactics other than #check.

[Eric Wieser]

Yaël Dillies said:

Would it be possible to put the squiggle on the characters past the limit only?

This linter is in mathlib, right? This feels like quite an easy PR.

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Restrict.20longLine.20warning.20to.20exceeding.20characters/near/547081669

[Eric Wieser]

Snir, it sounds like your complaint might lean further towards "some mathlib linters are annoying for development" than "the warning UI is bad"

[Snir Broshi]

Eric Wieser said:

Snir, it sounds like your complaint might lean further towards "some mathlib linters are annoying for development" than "the warning UI is bad"

Yeah but I don't want to turn them off completely, even for development. The gutter is a pretty good middle-ground for me, although the fact that it can't support hovers kinda ruins this idea.

Usually when programming my preferred solution is to hide all warnings/errors on the current line, but in Lean I have many comments lines over the limit. Turning the line-limit linter off will mean I might miss long lines when opening a PR.

btw sorrys colored in red is a great choice :handshake:, I don't miss the yellow squiggly on theorem names as I can easily see when a theorem uses sorry.