Making the `minImports` linter support file editing

Stream: mathlib4

[Anne Baanen]

So yesterday I tried making the minImports linter continue working when editing a file, and I made #18914 which almost works. The idea is that we want to know for each piece of syntax that the linter runs on, what the result was of running the linter on the previous syntax item. Currently, this is done by updating an IORef for the file, which works only if the declarations are elaborated top to bottom.

In #18914 I instead tried to work by syntax position: check the starting position of the syntax we are elaborating, and then look up the last result with ending position before that point. The problem is that by pasting or deleting code in a tricky way, we can end up with the situation that we have a new declaration that has its start position before an old declaration's end position, so the linter gets confused.

Does anyone have suggestions for how to make a robust fix?

[Anne Baanen]

One thing that would work much better is, given a piece of syntax, to look up the command immediately preceding it.

[Anne Baanen]

I don't think that docs#Lean.DeclarationRanges would be exactly the right way to go, since the linter runs on commands, not necessarily named declarations.

[Anne Baanen]

And I suppose reparsing the file for each call to the linter would also be an issue...

[Damiano Testa]

I would really like to see a solution to this question, since I had also tried to circumvent these issues, but failed. I find that having a way of consistently "passing information" between declarations when running a linter is always tricky.

[Kim Morrison]

I think the right conclusion here is:

• passing information between linters is a bad idea for now, and given the demands of parallelism it's unlikely we'll add support for this
• allowing a linter to see that syntax/source of everything up to the current definition seems plausible (although again, maybe made more complicated by parallelism)
• @Damiano Testa, perhaps you could write an RFC on the lean4 repository asking for a mechanism for a linter to see everything up to the current definition?

[Damiano Testa]

lean4#6076

[Damiano Testa]

Comments on the request for comments are welcome! :smile: