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

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 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the referenced Mathlib/Tactic/Linter/Header.lean and Mathlib/Tactic/Linter/MinImports.lean workarounds, then review the linked Zulip discussions and mathlib pull request. A completed effort would define and implement a reliable way for linters to access syntax through the current command, with its behavior and limitations documented.