feat: lake: read recorded code quality metrics in lake lint

[wkrozowski]

This PR makes lake lint --code-quality emit the code quality entries recorded during elaboration (via Lean.Linter.logCodeQualityEntry) alongside the linter-derived and package-check ones. Recorded entries are now attributed to the linter option that produced them, so --lint-only restricts them in the same way as ordinary linter warnings.

Lean.Linter.logCodeQualityEntry now takes the producing linter's option and tags its message with the option name, mirroring logLint. Lean.Linter.recordLints persists that name together with the entry in codeQualityLogExt (as the new CodeQualityLogEntry) and drops entries that carry no linter tag. lake lint recovers the entries from the .oleans of each lint target's package modules without re-elaboration, filters them under --lint-only via the recorded linter name, and collects a module's entries only once when it appears in several targets' import closures.

[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 af46668adab413eed68e9921ad19996fc7312924 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 16:03:30)

[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 af46668adab413eed68e9921ad19996fc7312924 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-20 16:03:32)