feat: do not export private declarations

[Kha]

This PR adjusts the experimental module system to not export any private declarations from modules.

Fixes #5002

[Kha]

!bench

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-8337 build failed against this PR. (2025-05-14 16:46:13) View Log

[leanprover-bot]

Here are the benchmark results for commit 58edbda.
There were significant changes against commit 29cc755:

  Benchmark                   Metric                 Change
  ====================================================================
+ Init size                   bytes .olean            -9.1%
- Init size                   bytes .olean.private     4.8%
+ bv_decide_inequality.lean   task-clock              -6.2%  (-21.5 σ)
+ bv_decide_inequality.lean   wall-clock              -5.9%  (-24.0 σ)
+ import Lean                 branches                -3.3%  (-89.9 σ)
+ import Lean                 instructions            -3.6%  (-89.3 σ)
+ import Lean                 maxrss                  -1.3%  (-77.5 σ)
+ import Lean                 task-clock             -10.9%  (-25.8 σ)
+ import Lean                 wall-clock             -10.9%  (-25.3 σ)
+ lake build clean            instructions            -1.1%  (-23.9 σ)
+ lake build clean            task-clock              -4.7%  (-43.0 σ)
+ lake build clean            wall-clock              -3.6%  (-21.7 σ)
+ lake config elab            instructions            -1.2%  (-76.1 σ)
+ lake config elab            maxrss                  -1.2%  (-29.2 σ)
+ lake config import          instructions            -2.5% (-192.3 σ)
+ lake config import          maxrss                  -2.5% (-143.3 σ)
+ lake config tree            instructions            -2.4%  (-34.8 σ)
+ lake config tree            maxrss                  -2.5%  (-47.9 σ)
+ lake env                    instructions            -2.5% (-124.2 σ)
+ lake env                    maxrss                  -2.5%  (-72.8 σ)
+ language server startup     branches                -1.3%  (-36.2 σ)
+ language server startup     instructions            -1.4%  (-32.5 σ)
- nat_repr                    branches                 1.4%  (247.0 σ)
- nat_repr                    instructions             1.4%  (194.8 σ)
+ stdlib                      maxrss                  -1.6% (-172.3 σ)
+ stdlib                      wall-clock              -2.5%  (-37.1 σ)
- stdlib size                 bytes .olean.private     4.8%
+ workspaceSymbols            maxrss                  -1.6%  (-25.2 σ)

[Rob23oba]

Since Thunk.fn is public now, maybe add

@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6886d98.
There were significant changes against commit 528fe0b:

  Benchmark     Metric                 Change
  ===========================================
+ Init size     bytes .olean.private    -2.4%
+ stdlib size   bytes .olean.private    -2.4%