From 5fff9fb22869d358b73109dbd77795c123b0eb99 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 12 Dec 2025 21:51:34 +0100 Subject: [PATCH] perf: remove obsolete old codegen workaround (#9311) --- src/Lean/CoreM.lean | 4 +--- src/Lean/Meta/Match/MatchEqs.lean | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 8abc09cf5d..ea97530d47 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -708,9 +708,7 @@ def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do -- `ref?` is used for error reporting if available partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do - -- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found - -- by the replay code - if !Elab.async.get (← getOptions) || (← getEnv).isRealizing then + if !Elab.async.get (← getOptions) then let _ ← traceBlock "compiler env" (← getEnv).checked doCompile return diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index bd1666f338..36baf9dab1 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -229,7 +229,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no assert! matchInfo.altInfos == splitterAltInfos -- This match statement does not need a splitter, we can use itself for that. -- (We still have to generate a declaration to satisfy the realizable constant) - addAndCompile <| Declaration.defnDecl { + addAndCompile (logCompileErrors := false) <| Declaration.defnDecl { name := splitterName levelParams := constInfo.levelParams type := constInfo.type