Skip to content

Commit 5fff9fb

Browse files
authored
perf: remove obsolete old codegen workaround (#9311)
1 parent 59045c6 commit 5fff9fb

File tree

2 files changed

+2
-4
lines changed

2 files changed

+2
-4
lines changed

src/Lean/CoreM.lean

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -708,9 +708,7 @@ def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do
708708

709709
-- `ref?` is used for error reporting if available
710710
partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do
711-
-- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found
712-
-- by the replay code
713-
if !Elab.async.get (← getOptions) || (← getEnv).isRealizing then
711+
if !Elab.async.get (← getOptions) then
714712
let _ ← traceBlock "compiler env" (← getEnv).checked
715713
doCompile
716714
return

src/Lean/Meta/Match/MatchEqs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -229,7 +229,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
229229
assert! matchInfo.altInfos == splitterAltInfos
230230
-- This match statement does not need a splitter, we can use itself for that.
231231
-- (We still have to generate a declaration to satisfy the realizable constant)
232-
addAndCompile <| Declaration.defnDecl {
232+
addAndCompile (logCompileErrors := false) <| Declaration.defnDecl {
233233
name := splitterName
234234
levelParams := constInfo.levelParams
235235
type := constInfo.type

0 commit comments

Comments
 (0)