chore: upstream Std's linter framework

[kim-em]

It is the second linter framework from Std. It runs after declarations have been made, and e.g. can verify global properties of simp sets.

WIP, there are a number of problems here:

• Where does this go?
• What namespace does it live in?
• The simp linter, which I've included here, uses open private to get access to simp internals.
• Do we actually want this? We could proceed without it for now, at the cost of separating some @[nolint] attributes from their declarations.

[kim-em]

To be discussed at the 12 Feb all-hands.

[digama0]

(For clarity, I will be calling the two linter frameworks "syntax linters" and "environment linters" from now on.)

Remark: In the last meeting we discussed the possibility of "finalizers" which can be registered similarly to syntax linters and trigger at the end of the file. It is possible that we can use finalizers as a substitute for environment linters, with the advantage that the linting results appear directly in the file instead of only in CI. The main downside is that if we were to do this with all of mathlib's linters it would have the effect of running linting at the same time as the build, which would mean lost parallelism unless we can generate the .olean file before running finalizers and signal to lake that it can continue with dependent files even though the lean process has not exited yet.

Some environment linters like simpNF are global analyses, which cannot run (only) at the end of each file. These would still have to be run in a separate step, and if we're upstreaming it then this would likely be a responsibility of lake (e.g. an additional kind of target).