perf: avoid unnecessary modifyEnv

[leodemoura]

This PR implements a minor optimization at withExporting/withoutExporting. When they call modifyEnv to toggle Environment.isExporting, and MonadEnv MetaM's modifyEnv wipes all Core and Meta caches.

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for c05ce98 against 4c1cf2f are in. There are significant results. @leodemoura

• ✅ build//instructions: -71.7G (-0.61%)

Large changes (4✅, 1🟥)

• 🟥 build/profile/interpretation//wall-clock: +1s (+1.23%)
• ✅ elab/grind_bitvec2//instructions: -5.0G (-3.46%)
• ✅ elab/grind_list2//instructions: -2.4G (-5.48%)
• ✅ vcgen/GetThrowSetGrind/200/vcgen//wall-clock: -38ms (-17.04%)
• ✅ vcgen/GetThrowSetGrind/300/vcgen//wall-clock: -55ms (-16.67%)

Medium changes (14✅)

• ✅ build//instructions: -71.7G (-0.61%)
• ✅ build/module/Init.Data.String.Decode//instructions: -1.1G (-3.75%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.77%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.8G (-1.10%)
• ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -4.4G (-2.87%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -3.7G (-1.61%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Model//instructions: -2.2G (-3.45%)
• ✅ build/module/Std.Http.Data.Headers.Name//instructions: -1.3G (-13.35%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: -2.3G (-5.64%) (reduced significance based on absolute threshold)
• ✅ elab/mut_rec_wf//instructions: -234.3M (-1.08%)
• ✅ elab/riscv-ast//instructions: -803.9M (-0.90%)
• ✅ lake/inundation/startup//maxrss: -5MiB (-4.75%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.8G (-1.26%)
• ✅ vcgen/GetThrowSetGrind/100/vcgen//wall-clock: -19ms (-15.83%)

and 1 hidden

Small changes (348✅, 3🟥)

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

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for 4680969 against da19ea0 are in. There are significant results. @leodemoura

• ✅ build//instructions: -72.1G (-0.65%)

Large changes (7✅)

• ✅ compiled/incr_header_load//instructions: -449.1M (-38.54%)
• ✅ compiled/incr_header_load//maxrss: -64MiB (-10.20%)
• ✅ compiled/incr_header_load//wall-clock: -78ms (-52.72%)
• ✅ elab/grind_bitvec2//instructions: -5.1G (-3.54%)
• ✅ elab/grind_list2//instructions: -2.4G (-5.50%)
• ✅ vcgen/GetThrowSetGrind/200/vcgen//wall-clock: -39ms (-17.41%)
• ✅ vcgen/GetThrowSetGrind/300/vcgen//wall-clock: -58ms (-17.68%)

Medium changes (12✅)

• ✅ build//instructions: -72.1G (-0.65%)
• ✅ build/module/Init.Data.String.Decode//instructions: -1.0G (-3.79%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.80%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.8G (-1.22%)
• ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -4.4G (-3.32%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -3.6G (-1.93%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Model//instructions: -2.2G (-3.51%)
• ✅ build/module/Std.Http.Data.Headers.Name//instructions: -1.3G (-13.63%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: -2.3G (-5.72%) (reduced significance based on absolute threshold)
• ✅ elab/mut_rec_wf//instructions: -250.6M (-1.15%)
• ✅ elab/riscv-ast//instructions: -824.7M (-0.93%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.8G (-1.26%)

and 1 hidden

Small changes (349✅, 4🟥)

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

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@d4f5e49 against leanprover-community/mathlib4-nightly-testing@d87691e are in. There are significant results. @leodemoura

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

• ✅ build//instructions: -1.3T (-0.82%)

Large changes (8✅)

• ✅ build//instructions: -1.3T (-0.82%)
• ✅ build/module/Mathlib.Algebra.Module.Torsion.PrimaryComponent//instructions: -24.4G (-36.53%)
• ✅ build/module/Mathlib.Algebra.MonoidAlgebra.PointwiseSMul//instructions: -9.9G (-39.04%)
• ✅ build/module/Mathlib.Algebra.Order.Monoid.Canonical.Basic//instructions: -9.7G (-30.25%)
• ✅ build/module/Mathlib.Analysis.Calculus.DerivativeTest//instructions: -10.8G (-18.16%)
• ✅ build/module/Mathlib.Geometry.Euclidean.Angle.Bisector//instructions: -15.2G (-18.65%)
• ✅ build/module/Mathlib.LinearAlgebra.Reflection//instructions: -11.6G (-19.51%)
• ✅ build/module/Mathlib.Topology.Sets.CompactOpenCovered//instructions: -13.8G (-25.49%)

and 1 hidden

Medium changes (36✅)

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

Small changes (189✅)

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

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14354 has successfully built against this PR. (2026-07-10 14:47:20) View Log
• 🟡 Reference manual branch lean-pr-testing-14354 build against this PR didn't complete normally. (2026-07-10 14:48:25) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14354 has successfully built against this PR. (2026-07-10 15:43:48) View Log