feat: extract simple array literals as static initializers

[hargoniX]

This PR implements support for extracting simple ground array literals into statically initialized data.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for a7dbf89 against 9843794 are in! @hargoniX

• ✅ build//instructions: -2.0G (-0.02%)

Large changes (3✅, 1🟥)

• ✅ compiled/binarytrees.st//instructions: -43.9M (-0.07%)
• 🟥 compiled/qsort//instructions: +192.7M (+1.15%)
• ✅ size/compile/.out//bytes: -27MiB (-1.40%)
• ✅ size/libleanshared.so//bytes: -879kiB (-0.61%)

Medium changes (1✅)

• ✅ compiled/hashmap//instructions: -3.4M (-0.09%)

Small changes (2✅, 4🟥)

• 🟥 build/module/Init.Data.Nat.SOM//instructions: +278.0M (+1.24%)
• 🟥 build/module/Lean.Compiler.IR.EmitC//instructions: +192.6M (+1.54%) (reduced significance based on *//lines)
• 🟥 compiled/liasolver//instructions: +2.8M (+0.07%)
• 🟥 compiled/unionfind//instructions: +3.0M (+0.01%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -7.6M (-1.02%)
• ✅ size/install//bytes: -5MiB (-0.23%)

[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 9843794e3f269b65bdce1fc72c373b77b8442750 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 14:00:16)

[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 9843794e3f269b65bdce1fc72c373b77b8442750 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 14:00:17)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for c15b0ca against 81a5eb5 are in! @hargoniX

• ✅ build//instructions: -1.6G (-0.01%)

Large changes (2✅, 1🟥)

• ✅ compiled/binarytrees.st//instructions: -35.0M (-0.05%)
• 🟥 compiled/qsort//instructions: +193.2M (+1.15%)
• ✅ size/compile/.out//bytes: -20MiB (-1.04%)

Medium changes (2✅)

• ✅ compiled/liasolver//instructions: -21.5M (-0.52%)
• ✅ size/libleanshared.so//bytes: -587kiB (-0.41%)

Small changes (2✅, 3🟥)

• 🟥 build/module/Lean.Compiler.IR.EmitC//instructions: +166.7M (+1.33%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Compiler.LCNF.SimpleGroundExpr//instructions: +1.8G (+26.36%) (reduced significance based on *//lines)
• ✅ compiled/hashmap//instructions: -2.2M (-0.06%)
• 🟥 compiled/unionfind//instructions: +4.8M (+0.02%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -6.1M (-0.82%)

[leanprover-radar]

Benchmark results for c15b0ca against 81a5eb5 are in! @hargoniX

• ✅ build//instructions: -1.6G (-0.01%)

Large changes (2✅, 1🟥)

• ✅ compiled/binarytrees.st//instructions: -35.0M (-0.05%)
• 🟥 compiled/qsort//instructions: +193.2M (+1.15%)
• ✅ size/compile/.out//bytes: -20MiB (-1.04%)

Medium changes (2✅)

• ✅ compiled/liasolver//instructions: -21.5M (-0.52%)
• ✅ size/libleanshared.so//bytes: -587kiB (-0.41%)

Small changes (2✅, 3🟥)

• 🟥 build/module/Lean.Compiler.IR.EmitC//instructions: +166.7M (+1.33%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Compiler.LCNF.SimpleGroundExpr//instructions: +1.8G (+26.36%) (reduced significance based on *//lines)
• ✅ compiled/hashmap//instructions: -2.2M (-0.06%)
• 🟥 compiled/unionfind//instructions: +4.8M (+0.02%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -6.1M (-0.82%)