feat: do not export def bodies by default

[Kha]

This PR adjusts the experimental module system to not export the bodies of defs unless opted out by the new attribute @[expose] on the def or on a surrounding section.

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit ab9a9cd.
There were significant changes against commit 70917fa:

  Benchmark                            Metric                  Change
  =================================================================================
+ Init size                            bytes .olean             -7.5%
- Init size                            bytes .olean.private      7.9%
+ Init.Data.BitVec.Lemmas re-elab      branch-misses           -99.3% (-324731.9 σ)
+ Init.Data.BitVec.Lemmas re-elab      branches                -99.3% (-300158.6 σ)
+ Init.Data.BitVec.Lemmas re-elab      instructions            -99.3% (-301915.5 σ)
+ Init.Data.BitVec.Lemmas re-elab      maxrss                  -67.3%    (-200.3 σ)
+ Init.Data.BitVec.Lemmas re-elab      task-clock              -99.4%  (-15275.4 σ)
+ Init.Data.BitVec.Lemmas re-elab      wall-clock              -96.7%   (-8615.6 σ)
+ Init.Data.List.Sublist re-elab -j4   branch-misses           -15.4%    (-805.7 σ)
+ Init.Data.List.Sublist re-elab -j4   instructions             -1.4%     (-92.9 σ)
+ Init.Data.List.Sublist re-elab -j4   maxrss                  -46.2%    (-452.5 σ)
+ Init.Data.List.Sublist re-elab -j4   task-clock              -18.4%    (-178.5 σ)
+ Init.Data.List.Sublist re-elab -j4   wall-clock               -3.6%    (-102.3 σ)
+ import Lean                          branches                 -3.1%   (-1638.7 σ)
+ import Lean                          instructions             -3.4%   (-1111.5 σ)
+ import Lean                          maxrss                   -1.3%     (-60.9 σ)
+ lake config elab                     instructions             -1.1%     (-55.0 σ)
+ lake config import                   instructions             -2.7%    (-175.8 σ)
+ lake config import                   maxrss                   -2.6%    (-266.9 σ)
+ lake config tree                     instructions             -2.5%     (-74.0 σ)
+ lake config tree                     maxrss                   -2.7%    (-106.3 σ)
+ lake env                             instructions             -2.6%    (-154.5 σ)
+ lake env                             maxrss                   -2.6%     (-96.9 σ)
+ language server startup              branches                 -1.1%     (-54.9 σ)
+ language server startup              instructions             -1.3%     (-51.1 σ)
- nat_repr                             branches                  1.5%     (164.6 σ)
- nat_repr                             instructions              1.4%     (136.6 σ)
- parser                               instructions              1.3%     (227.9 σ)
+ rbmap_library                        task-clock               -4.7%     (-34.3 σ)
+ rbmap_library                        wall-clock               -4.7%     (-29.6 σ)
+ stdlib                               attribute application    -2.3%   (-1001.0 σ)
- stdlib size                          bytes .olean.private      7.9%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2a5eb48.
There were significant changes against commit 70917fa:

  Benchmark                            Metric                    Change
  ================================================================================
+ Init size                            bytes .olean               -7.5%
- Init size                            bytes .olean.private        7.9%
+ Init.Data.List.Sublist re-elab -j4   branch-misses             -15.1%  (-63.6 σ)
+ Init.Data.List.Sublist re-elab -j4   maxrss                    -46.2% (-116.9 σ)
+ Init.Data.List.Sublist re-elab -j4   task-clock                -17.9% (-204.2 σ)
+ Init.Data.List.Sublist re-elab -j4   wall-clock                 -3.3%  (-38.9 σ)
+ bv_decide_mul                        wall-clock                 -3.0%  (-21.6 σ)
+ import Lean                          branches                   -3.1% (-210.2 σ)
+ import Lean                          instructions               -3.4% (-224.2 σ)
+ import Lean                          maxrss                     -1.3% (-177.0 σ)
+ lake config elab                     instructions               -1.2% (-137.5 σ)
+ lake config import                   instructions               -2.7% (-130.1 σ)
+ lake config import                   maxrss                     -2.6% (-953.8 σ)
+ lake config tree                     instructions               -2.4% (-111.4 σ)
+ lake config tree                     maxrss                     -2.6%  (-73.8 σ)
+ lake env                             instructions               -2.6%  (-92.4 σ)
+ lake env                             maxrss                     -2.6%  (-30.9 σ)
+ language server startup              branches                   -1.1%  (-30.4 σ)
+ language server startup              instructions               -1.2%  (-32.6 σ)
- nat_repr                             branches                    1.4%  (187.1 σ)
- nat_repr                             instructions                1.4%  (157.3 σ)
- parser                               instructions                1.3%  (220.4 σ)
+ simp_arith1                          branches                   -1.5%  (-29.1 σ)
+ simp_arith1                          instructions               -1.6%  (-28.0 σ)
+ stdlib                               maxrss                     -1.3% (-213.5 σ)
+ stdlib                               process pre-definitions    -1.0%  (-45.1 σ)
+ stdlib                               task-clock                 -1.4%  (-42.2 σ)
- stdlib size                          bytes .olean.private        7.9%
+ tests/bench/ interpreted             maxrss                     -1.4%  (-50.9 σ)

[Kha]

!bench

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6eafff7.Found no runs to compare against.