feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies

[Kha]

This PR adds the necessary infrastructure for recording elaboration dependencies that may not be apparent from the resulting environment such as notations and other metaprograms. An adapted version of shake from Mathlib is added to script/ but may be moved to another location or repo in the future.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 74260e2.
There were significant changes against commit 69c8f13:

  Benchmark                 Metric                    Change
  =====================================================================
+ binarytrees.st            maxrss                     -9.7%  (-61.2 σ)
- bv_decide_rewriter.lean   branches                    1.9%   (83.1 σ)
- bv_decide_rewriter.lean   instructions                1.3%   (41.1 σ)
- lake config elab          instructions                2.5%   (91.7 σ)
- libleanshared.so          binary size                 1.0%
- mut_rec_wf                branches                    1.9%  (119.7 σ)
- mut_rec_wf                instructions                1.2%   (77.8 σ)
- stdlib                    attribute application       1.5%   (50.2 σ)
- stdlib                    blocked (unaccounted)      12.3%   (26.6 σ)
- stdlib                    grind ematch                4.2%   (47.2 σ)
- stdlib                    process pre-definitions     1.3%   (27.8 σ)
+ unionfind                 maxrss                     -7.2% (-178.9 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit bfe28ae.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 48a67f5.
There were significant changes against commit 69c8f13:

  Benchmark                   Metric                  Change
  =====================================================================
+ binarytrees.st              maxrss                   -9.6%  (-59.7 σ)
- bv_decide_inequality.lean   maxrss                    1.4%   (20.6 σ)
- stdlib                      blocked (unaccounted)    12.8%   (27.9 σ)
+ treemap.lean                insertHit                -1.2%  (-60.7 σ)
+ unionfind                   maxrss                   -7.2% (-342.9 σ)

[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 69c8f13bf21a4a86000ca9f3f7288fad579de45b --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 19:22:02)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-28 14:23:08)

[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 69c8f13bf21a4a86000ca9f3f7288fad579de45b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 19:22:04)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-28 14:23:09)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 96abc1b.
There were significant changes against commit 9b1109c:

  Benchmark                 Metric                  Change
  ==================================================================
- Init.Data.BitVec.Lemmas   task-clock                4.7%  (52.5 σ)
+ grind_ring_5.lean         branch-misses            -4.6% (-28.5 σ)
+ mut_rec_wf                branch-misses            -2.4% (-25.0 σ)
+ riscv-ast.lean            branch-misses            -2.6% (-55.0 σ)
- stdlib                    blocked (unaccounted)    13.7%  (29.4 σ)
+ stdlib                    grind ac                 -4.3% (-36.4 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit e7d2354.
There were significant changes against commit 9b1109c:

  Benchmark   Metric          Change
  =============================================
+ stdlib      type checking    -1.6% (-134.5 σ)