perf: non quadratic closed term initialization for closed array literals

[hargoniX]

This PR ensures the compiler extracts Array/ByteArray/FloatArray literals as one big closed term to avoid quadratic overhead at closed term initialization time.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for a90890b against adf3e5e are in! @hargoniX

• ✅ build//instructions: -5.1G (-0.04%)

Large changes (1✅)

• ✅ size/compile/.out//bytes: -18MiB (-0.93%)

Small changes (17✅, 1🟥)

• 🟥 build/module/Lean.Compiler.LCNF.ExtractClosed//instructions: +788.1M (+21.69%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Compiler.LCNF.Passes//instructions: -23.2M (-1.03%)
• ✅ build/module/Lean.Data.Json.Printer//instructions: -128.6M (-2.90%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: -191.4M (-0.53%)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Simproc//instructions: -69.9M (-1.22%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec//instructions: -190.6M (-1.85%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char//instructions: -30.7M (-1.05%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin//instructions: -109.8M (-1.72%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int//instructions: -65.8M (-1.23%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat//instructions: -65.2M (-0.86%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt//instructions: -176.8M (-0.86%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.String//instructions: -26.2M (-1.09%)
• ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt//instructions: -157.5M (-1.05%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Server.ProtocolOverview//instructions: -33.7M (-1.73%)
• ✅ compiled/rbmap_library//instructions: -2.6M (-0.03%)
• ✅ lake/inundation/startup//instructions: -2.2M (-1.11%)
• ✅ size/all/.ir//bytes: -852kiB (-0.26%)
• ✅ size/install//bytes: -5MiB (-0.21%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for adde160 against 738688e are in! @hargoniX

• ✅ build//instructions: -231.7M (-0.00%)

Large changes (1✅)

• ✅ size/compile/.out//bytes: -25MiB (-1.31%)

Medium changes (1🟥)

• 🟥 elab/simp_local//instructions: +233.8M (+0.52%)

Small changes (21✅, 3🟥)

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 738688efeed68cd70c7ae8a51e07d63e0095b73e --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 00:07:57)

[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 738688efeed68cd70c7ae8a51e07d63e0095b73e --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 00:07:58)