diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 8abc09cf5d46..ea97530d4711 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 bd1666f338a8..36baf9dab154 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