feat: meta phase restrictions

[Kha]

This PR extends the experimental module system with a phase distinction between meta and regular declarations. This distinction will be used in follow-up PRs to avoid importing IR that is not needed for compile-time execution.

The phase distinction system deliberately is the weakest one to implement this goal:

• meta declarations may use any local declaration, imported meta declarations, and any meta imported declarations.
• non-meta declarations may use a non-meta declaration reachable only through non-meta imports.

Thus it is allowed and can be necessary to import the same module into both the meta and regular phase via two separate import statements. meta import is transitive in the sense that importing a meta import is the same as writing the meta import inline.

Based on #8653

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d46188de54f86c64cef85aaba800f4171ccffcd5 --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-07 15:35:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54c12df9509d639ad78fb1343b13c60370a9481d --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 14:32:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0002ea8a3702a0c2191b03e1274aefc05b53ca8c --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 15:54:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d10a85539a911ea2b76eb91b0d47957c35d22587 --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 13:32:08)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit b32e48b.
There were significant changes against commit d46188d:

  Benchmark                            Metric          Change
  =====================================================================
+ Init.Data.BitVec.Lemmas re-elab      branch-misses    -1.6% (-34.3 σ)
- Init.Data.List.Sublist re-elab -j4   task-clock        1.3%  (27.3 σ)
- Init.Data.List.Sublist re-elab -j4   wall-clock        2.0% (105.4 σ)
+ workspaceSymbols                     task-clock       -3.3% (-48.7 σ)
+ workspaceSymbols                     wall-clock       -3.3% (-51.4 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9f5e6e0.
There were significant changes against commit 54c12df:

  Benchmark                            Metric       Change
  ==================================================================
- Init.Data.List.Sublist re-elab -j4   branches       1.2%  (20.3 σ)
+ stdlib                               wall-clock    -1.0% (-37.4 σ)