RFC : make `omit ... in` vscode hint a quickfix

Stream: lean4

[Shreyas Srinivas]

With the recent changes in the behaviour of variable we seem to get hints about including or omitting section variables as shown in the screenshot
Screenshot from 2024-10-31 15-43-58.png

Can we get these as automatic vscode quick-fixes instead?

CC : @Marc Huisinga

[Kim Morrison]

The problem is that omit is intended as "last resort", and reorganizing is hard to do automatically.

[Shreyas Srinivas]

But it doesn't need to. The LSP is already suggesting the line omit ... in

[Shreyas Srinivas]

It just needs to insert the line

[Shreyas Srinivas]

Or offer a quickfix option to do that

[Shreyas Srinivas]

Like Haskell does

[Kim Morrison]

What I am saying is that that is not the preferred solution, so we should not provide a code action, because that would encourage users to do the non-preferred thing.

[Shreyas Srinivas]

Okay I see. But what's the preferred way to handle this? Not have variables? Or use sections more often?

I put these typeclass variable declarations of Fintyoe and DecidableEq on top of the namespace because for the topic, these are true by definition throughout this subfield of discrete fair division.

[Kim Morrison]

Yes, more sections, possibly rearranging lemmas so that the variables are required for shorter scopes.

It's not perfect, but there was a lot of problems and dissatisfaction with the previous variables behaviour!

[Eric Wieser]

Kim Morrison said:

What I am saying is that that is not the preferred solution, so we should not provide a code action, because that would encourage users to do the non-preferred thing.

How about if the code action emitted

-- TODO: remove `omit in` and move to another section instead
omit [Foo x] [Bar x] in

[Shreyas Srinivas]

I like this idea. I am currently tempted to just disable this linter altogether, because creating sections to handle this while developing lemmas is a bit tedious

[Jireh Loreaux]

Eric, that would be a hindrance to trying to track / eliminate TODOs in Mathlib.

[Shreyas Srinivas]

I don't see the disadvantage os using omit over tedious rearrangement and sectioning

[Shreyas Srinivas]

My preference might be because in general I favour organising code for semantic reasons. Not tooling issues

[Eric Wieser]

Jireh Loreaux said:

Eric, that would be a hindrance to trying to track / eliminate TODOs in Mathlib.

We'd reject them in review, but the point is that the options you have now are:

1. Ignore the warning, and end up with theorems with extra assumptions that will trip you up later
2. Do the resectioning immediately, which is a annoying while trying to prove things
3. Copy the omit ... in command from the infoview (which can also be annoying), and come back to it later

While you should obviously do 2 before contributing to mathlib, while developing 3 is less of a footgun than 1, and so we should make it as easy as possible.

[Shreyas Srinivas]

(deleted)