feat: add module syntax linters

[wkrozowski]

This PR adds module linters, which run once at the end of elaborating a module rather than after every command. A module linter receives the full array of top-level command syntaxes for the module, making it suitable for checks that need a whole-module view (e.g. enforcing module-wide syntactic conventions) rather than per-command checks.

A module linter is a value of the new Lean.Elab.Command.ModuleLinter structure, registered via addModuleLinter (analogous to Linter/addLinter). Registered linters are stored in a moduleLintersRef and
dispatched from runLintersAsync when the current command is a terminal command, as determined by Parser.isTerminalCommand (Command.exit, Command.import, Command.eoi). The accumulated commands array is threaded through Language.Lean.parseCmd and doElab and passed into elabCommandTopLevel, so a module linter sees every top-level command parsed in the module. A new package test under tests/pkg/module_linter registers a dummy module linter and asserts that it sees the full command sequence.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ceba2934266d45599eaf3df0b868b00550bf893d --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-01 18:00:00)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ceba2934266d45599eaf3df0b868b00550bf893d --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-01 18:00:02)