withSetOptionIn improvement?

Stream: lean4

[Damiano Testa]

There is a behaviour that I have come to accept about docs#Lean.withSetOptionIn but that I think could be improved.

[Damiano Testa]

withSetOptionIn is used by virtually all mathlib linters and also some core ones and recursively peels off set_option ... in at the start of a command, before linting the "inner" command with the appropriate options set.

[Damiano Testa]

The behaviour that I would like, though is that it would see through all set_option ... in, even if they are not the outermost.

[Damiano Testa]

Here is an example.

import Lean.Linter.List

-- warning present
set_option linter.indexVariables true in
variable (a : Nat) (l : List Unit) in
example : l[a]? = l[a]? := rfl

-- warning not present
variable (a : Nat) (l : List Unit) in
set_option linter.indexVariables true in
example : l[a]? = l[a]? := rfl

[Damiano Testa]

In the first example, the outermost set_option is correctly processed, the linter sees through it and activates itself in the included command.

[Damiano Testa]

In the second example, withSetOptionIn does nothing, since the outermost modifier is variable, which means that the set_option does not get applied to the resulting command and the linter stays off.

[Damiano Testa]

Would it be possible to get withSetOptionIn to see through "all" modifiers? Or at least the common ones, like open, variable, maybe also include and omit?

[Thomas Murrills]

(At the very least, we could have a linter which alerts the user to any unused set_option linter.foo _ ins throughout the syntax…but if it can be done in a way that makes sense, actually processing the set_options would definitely be much better! :grinning_face_with_smiling_eyes:)

[Damiano Testa]

The unnecessary set_option_in linter is #13653, but I do not remember when the last time that I used was...

[Michael Rothgang]

I've made #31188 which runs it on current master. Help fixing any true issues it finds is welcome!

[Thomas Murrills]

Damiano Testa said:

The unnecessary set_option_in linter is #13653, but I do not remember when the last time that I used was...

Ah, nice! This is a "heavy-duty" approach which elaborates the command multiple times, and compares the difference, right? This is definitely great for its purpose/running once in a while, but I'm wondering if we can have a lightweight always-running linter that checks for set_options which are definitely irrelevant too.

[Damiano Testa]

Yes, this was one of my experiment with understanding linters. With respect to speed, I think that it only acts on syntax that starts with set_option ... in so it should be quick for most declarations. It also never really worked well for heartbeats, so maybe it could exclude those by default.

Anyway, a better tool would be great!

[Thomas Murrills]

Some initial thoughts here on the actual topic:

• The obvious issue is that a few linters will want to lint in-modifiers like variable ... in, or will want to lint certain in-modifiers (e.g. "just variable). Maybe we could use some API to make processing set_option up to certain in-modifiers convenient, and let those opt-in to that approach, since...
• ...Many linters will want to discard all in modifiers. I agree we should make this convenient!
• Some linters will want to go even further, and traverse the syntax tree to find the target of their linting action. Is there API for handling term and tactic mode set_option properly when doing this? I don't believe I've seen it, but I might just be unaware.

So to summarize, I think we've got three cases:

• Linters that want to lint in-modifiers, broken down into
  • Linters that want to target specific in modifers
  • Linters that might target any in modifier
• Linters that want to lint the body of a command, and want to skip all in-modifiers
• Linters that traverse the syntax tree, potentially linting anything (terms, tactics, etc.)

Maybe this kind of breakdown (if we agree it's comprehensive!) can help us figure out what withSetOptionIn-like tools should be available. :)

[Thomas Murrills]

(And, likewise, if we record what category each linter falls into, we can do cheap linting for "definitely useless" set_options. E.g. a term-mode invocation of set_option linter.foo in definitely won't be used for a command-body linter, etc.)

[Damiano Testa]

Before making it so granular, I think that already extracting from a syntax term the maximalminimal subtrees that are themselves commands could be useful. If those came with a memory of the state of the relevant monads/environment, that would be even better!

[Damiano Testa]

If someone is interested in inspecting various combinations of modifiers, it seems fair to let them be on their own!