feat: lake: read persisted code quality entries in lake lint --code-quality

[wkrozowski]

This PR makes lake lint --code-quality emit the code quality entries that linters record during elaboration. Entries logged via Lean.Linter.logCodeQualityEntryIf are attributed to the producing linter's option name and are filtered by --lint-only; entries logged via Lean.Linter.logCodeQualityEntry carry no attribution and are always emitted, so no linter selection flag can suppress them. Disabling a recording linter (e.g. --linters=-linter.foo) suppresses its attributed entries at elaboration time, and a module shared between several lint targets contributes its entries only once.

Builds on #14914, which persists code quality entries in the codeQualityLogExt environment extension. The extension now stores CodeQualityLogEntry, pairing each entry with the option name of the producing linter (none for entries logged unconditionally via logCodeQualityEntry). On the Lake side, collectRecordedCodeQuality recovers the per-module entries from the .oleans of each lint target's import closure and applies the --lint-only filter to attributed entries. The now-dead MessageData.codeQualityEntry? and the unused Lean.Linter.CodeQuality.Basic import in Lean.Message are removed.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for a6dbd03 against 31aea96 are in. There are significant results. @wkrozowski

• ✅ build//instructions: -47.9G (-0.41%)

Large changes (3✅)

• ✅ build/stat/imported bytes//bytes: -2GiB (-7.00%)
• ✅ build/stat/imported consts//amount: -2.6M (-2.95%)
• ✅ build/stat/imported modules//amount: -424.3k (-19.48%)

Small changes (551✅, 4🟥)

• 🟥 build/module/Lake.CLI.BuiltinLint//instructions: +209.6M (+3.48%) (reduced significance based on *//lines)
• ✅ build/module/Lake.DSL.Attributes//instructions: -56.9M (-6.09%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.DSL.AttributesCore//instructions: -57.4M (-4.51%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.Util.Message//instructions: -62.6M (-6.52%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.Util.OrderedTagAttribute//instructions: -55.9M (-4.78%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.AddDecl//instructions: -55.2M (-0.98%)
• ✅ build/module/Lean.Attributes//instructions: -70.1M (-1.32%)
• ✅ build/module/Lean.AutoDecl//instructions: -56.5M (-5.01%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.BuiltinDocAttr//instructions: -57.9M (-5.44%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Class//instructions: -59.3M (-2.77%)
• ✅ build/module/Lean.Compiler.CSimpAttr//instructions: -57.2M (-2.96%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.ExportAttr//instructions: -56.5M (-5.66%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.ExternAttr//instructions: -60.2M (-2.79%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.IR.Basic//instructions: -66.1M (-1.04%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.IR.Checker//instructions: -66.3M (-2.38%)
• ✅ build/module/Lean.Compiler.IR.CompilerM//instructions: -65.6M (-2.86%)
• ✅ build/module/Lean.Compiler.IR.EmitUtil//instructions: -65.8M (-3.90%)
• ✅ build/module/Lean.Compiler.IR.Format//instructions: -61.9M (-2.40%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.IR.Meta//instructions: -59.1M (-4.18%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Compiler.IR.NormIds//instructions: -58.9M (-2.49%)
• and 534 more
• and 1 hidden