We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5778a3c commit 62a615fCopy full SHA for 62a615f
src/Lean/CoreM.lean
@@ -682,9 +682,7 @@ opaque compileDeclsImpl (declNames : Array Name) : CoreM Unit
682
683
-- `ref?` is used for error reporting if available
684
partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do
685
- -- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found
686
- -- by the replay code
687
- if !Elab.async.get (← getOptions) || (← getEnv).isRealizing then
+ if !Elab.async.get (← getOptions) then
688
let _ ← traceBlock "compiler env" (← getEnv).checked
689
doCompile
690
return
0 commit comments