perf: remove obsolete old codegen workaround (#9311)

This commit is contained in:
Sebastian Ullrich 2025-12-12 21:51:34 +01:00 committed by GitHub
parent 59045c6227
commit 5fff9fb228
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 2 additions and 4 deletions

View file

@ -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

View file

@ -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