From dac73c15c8d502c48957dcef9c7600235d2842fc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 8 Nov 2024 16:37:39 +0100 Subject: [PATCH] perf: avoid negative environment lookup (#5429) Avoids some `Environment.find?` lookup misses that become especially expensive on the async branch --- src/Lean/Meta/WHNF.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 55db7b40d4..e3eb695a76 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -831,10 +831,12 @@ mutual else unfoldDefault () | .const declName lvls => do + let some cinfo ← getUnfoldableConstNoEx? declName | pure none + -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a + -- significant chance of not existing and `Environment.contains` misses are more costly if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then return none else - let some cinfo ← getUnfoldableConstNoEx? declName | pure none unless cinfo.hasValue do return none deltaDefinition cinfo lvls (fun _ => pure none)