From af20c826cd70950637e37b6aecb41bb1b413f9c7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 29 Aug 2026 13:30:22 +0000 Subject: [PATCH] perf: avoid `setTransparency` when the transparency is already in effect This PR speeds up elaboration by not rebuilding the `MetaM` context when `withTransparency` or `withAtLeastTransparency` is asked for the transparency setting that is already in effect. `Context.setTransparency` rebuilds `Config`, `ConfigWithKey` and `Context`, so each such call allocated three objects and retraced the `Context`'s pointer fields even when nothing changed. `withTransparency` did this unconditionally, and `withAtLeastTransparency` did it by construction on the branch where the ambient mode already suffices. Both are hot: `withInferTypeConfig` wraps every `inferType` in `withAtLeastTransparency .default`, as does `getFunInfoAux`, and `.default` is usually the ambient mode already. Skipping the rebuild is observationally equivalent: `ConfigWithKey.key` is maintained as `Config.toKey`, whose low three bits are exactly `transparency.toUInt64`, so re-applying the current mode reproduces an identical `Config` and an identical key. Measured over 12 `elab_bench` files, 5 interleaved repetitions per variant against a same-machine baseline build: -0.33% instructions overall, with every file improving (-0.06% to -1.16%). The run-to-run noise floor for this metric is 0.10% per file and 0.00% overall. Co-Authored-By: Claude Opus 5 (1M context) --- src/Lean/Meta/Basic.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index e207f8f137bd..1791b62f7fde 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1304,8 +1304,10 @@ private def Context.setTransparency (ctx : Context) (transparency : Transparency { ctx with keyedConfig := ctx.keyedConfig.setTransparency transparency } @[inline] def withTransparency (mode : TransparencyMode) : n α → n α := - -- We avoid `withConfig` for performance reasons. - mapMetaM <| withReader (·.setTransparency mode) + -- We avoid `withConfig` for performance reasons. `setTransparency` rebuilds `Config`, + -- `ConfigWithKey` and `Context`, so skip it when the mode is already in effect. + mapMetaM <| withReader fun ctx => + if ctx.config.transparency == mode then ctx else ctx.setTransparency mode /-- `withDefault x` executes `x` using the default transparency setting. -/ @[inline] def withDefault (x : n α) : n α := @@ -1338,8 +1340,7 @@ Recall that `.none < .reducible < .instances < .implicit < .default < .all`. -/ @[inline] def withAtLeastTransparency (mode : TransparencyMode) : n α → n α := mapMetaM <| withReader fun ctx => - let modeOld := ctx.config.transparency - ctx.setTransparency <| if modeOld.lt mode then mode else modeOld + if ctx.config.transparency.lt mode then ctx.setTransparency mode else ctx /-- Execute `x` allowing `isDefEq` to assign synthetic opaque metavariables. -/ @[inline] def withAssignableSyntheticOpaque (x : n α) : n α :=