RFC: give linters access to all the syntax up to the current command

[adomani]

Proposal

• User Experience: How does this feature improve the user experience?

  Working with linters, I often would like to access the whole syntax structure of the module until the current position.

  For instance, this would make identifying the first non-import command easy (mathlib's Header linter would use this to check that every file starts with a module doc -- see in particular this workaround).

  For another example, mathlib's MinImports linter progressively accumulates minimum import requirements helping to split large files and reduce unnecessary import dependencies (see this brittle use of an IO.Ref to try to emulate a "linter memory", mathlib's PR mathlib4#18914 and the associated Zulip thread).

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

  As argued above, Mathlib would have immediate use of this feature.

• Maintainability: Will this change streamline code maintenance or simplify its structure?

  I am not sure about maintainability. I am aware of efforts to make elaboration of files no longer linear, and I imagine that this may cause problems at the time of passing the module syntax up to a given point reliably.

Community Feedback

Besides the Zulip thread mentioned above, this had already come up on Zulip here.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[Kha]

Likely this should be done by giving linters access to the entire snapshot tree; they are closer to language server request handlers than elaborators anyway.

[Kha]

RFC accepted!

[adomani]

Wonderful! This is great!

[adomani]

Also, I am not really sure how I could help, but I am happy to be of any assistance, e.g. by trying out potential solutions in some test cases that I have!