feat: control environment linters via Lean.Option

[wkrozowski]

This PR is work-in-progress proof-of-concept implementation of controlling builtin environment linters using Lean.Option.

Current prototype has been generate by Claude Opus.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 9e41e5f against cc503a5 are in. There are significant results. @wkrozowski

• 🟥 build//instructions: +5.1G (+0.05%)

Small changes (5✅, 17🟥)

Too many entries to display here. View the full report on radar instead.

[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 cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-28 17:18:12)

[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 cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-28 17:18:14)

[wkrozowski]

The vibe-coded prototype, has been manually re-implemented in #13893.