feat: use static initializers where possible

[hargoniX]

This PR makes the compiler produce C code that statically initializes close terms when possible. This change reduces startup time as the terms are directly stored in the binary instead of getting computed at startup.

The set of terms currently supported by this mechanism are:

• string literals
• ctors called with other statically initializeable arguments
• Name.mkStrX and other Name ctors as they require special support due to their computed field and occur frequently due to name literals.

In core there are currently 152,524 closed terms and of these 103,929 (68%) get initialized statically with this PR. The remaining 48585 ones are not extracted because they use (potentially transitively) various non trivial pieces of code like stringToMessageData etc. We might decide to add special support for these in the future but for the moment this feels like it's overfitting too much for core.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 4b631c1 against d8fb702 are in! @hargoniX

• ✅ build//instructions: -27.6G (-0.2%)

Large changes (3✅, 2🟥)

• 🟥 binarytrees.st//instructions: +119.1M (+0.2%)
• ✅ lake startup//instructions: -16.1M (-6.2%)
• 🟥 size/libleanshared.so//bytes: +7MiB (+3.4%)
• ✅ tests/compiler//sum binary sizes: -13.9M (-1.1%)
• ✅ unionfind//instructions: -22.1M (-0.1%)

Medium changes (8✅)

• ✅ hashmap.lean//instructions: -7.9M (-0.2%)
• ✅ iterators (compiled)//instructions: -2.3M (-0.5%)
• ✅ iterators (elab)//instructions: -15.4M (-0.5%)
• ✅ lake config tree//instructions: -51.9M (-3.3%)
• ✅ language server startup//instructions: -30.9M (-6.6%)
• ✅ nat_repr//instructions: -829.8M (-19.6%)
• ✅ rbmap_library//instructions: -17.2M (-0.1%)
• ✅ treemap.lean//instructions: -8.5M (-0.0%)

Small changes (1056✅, 15🟥)

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