unused simp argument linter feedback

Stream: general

[Yaël Dillies]

@Joachim Breitner, I have some feedback about the new unused simp linter:

1. It is truly amazing :heart:
2. When there are several unused simp lemma in the same simp call/same proof/neighboring proofs, fixing linter warnings starts feeling like a game of memory: As soon as you perform one suggested edit, all linter warnings disappear and you either have to wait a minute for the declaration to reload (yes, my proofs are a bit eh... :grimacing:) or you start editing blindly with what you remember.
3. There seems to be one Try this suggestion per extraneous lemma in a simp call, instead of one suggestion per simp call. This exacerbates the previous point.

[Ruben Van de Velde]

For 2 with proofs of different theorems: always work up from the last warning in the file

[Joachim Breitner]

Can I just stop reading after 1? :-)

[Joachim Breitner]

I chose to display a separate warning for each unused argument. This means that the user has to click multiple times to remove all of them (and wait for re-elaboration in between). But this just means multiple endorphine kicks, and the main benefit over a single warning that would have to span the whole argument list is that already the squigglies tell the users about unused arguments.

[Joachim Breitner]

I guess one could have multiple diagnosis, one per unused simp argument, and all of them offer the same all-removing hint? But that looks odd in the InfoView as well

[Malvin Gattinger]

When I had a lot of unused simps in slow proofs I changed the setting of vs code to be slower in updating the UI - not sure if it was the default LSP UI or the "ErrorLens" extension, but eventually I managed to edit fast enough to still see a few squiggly lines before they would have to be re-generated.

And I have a related but more general question: Is there a "accept all linter hints in this file" function or how hard would it be to make that?

[Joachim Breitner]

We don't have that yet, and I also hope we get it eventually. Ideally not only in VSCode but also in batch mode (so that you can update many files in one go)

[Yaël Dillies]

Joachim Breitner said:

the main benefit over a single warning that would have to span the whole argument list is that already the squigglies tell the users about unused arguments

Aha, so a single warning has to correspond to a single contiguous squiggle? That's a bit unfortunate here

[Joachim Breitner]

I could also try to add a second hint labeled “remove all unused simp arguments” if there is more than one. Probably this hint wouldn't show the diff (to be considerate of the screen space).

[Eric Wieser]

Are non-contiguous squiggles under consideration?

[Eric Wieser]

I had previously thought you could get them by attaching your message to mkNullNode #[part1, part2]

[Joachim Breitner]

Hmm, maybe I simply didn't know about that trick.

[Joachim Breitner]

But in LSP a diagnostic has a range, not a list of ranges, so I'm not too hopeful:
https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnostic

[Eric Wieser]

I guess the diagnostic could be duplicated for lsp, but maybe working around the protocol is unwise