diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 1356a0a4b4..4579073511 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -94,6 +94,7 @@ builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassMan addImportedFn := fun ns => return ([], ← ImportM.runCoreM <| runImportedDecls ns) addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew) exportEntriesFn := fun s => s.1.reverse.toArray + asyncMode := .sync } def getPassManager : CoreM PassManager := diff --git a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean index b950aec8ba..5551fb028c 100644 --- a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean +++ b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean @@ -410,6 +410,7 @@ builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEnt return ([], folders.switch) addEntryFn := fun (entries, map) entry => (entry.toFolderOleanEntry :: entries, map.insert entry.declName entry.folder) exportEntriesFn := fun (entries, _) => entries.reverse.toArray + asyncMode := .sync } def registerFolder (declName : Name) (folderDeclName : Name) : CoreM Unit := do diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 8b4468cd47..b63556c355 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -85,6 +85,7 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt addEntryFn := SpecState.addEntry addImportedFn := fun _ => {} toArrayFn := fun s => sortEntries s.toArray + asyncMode := .sync } /-- diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 2c01478708..ec626d3b5f 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -32,6 +32,7 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache registerSimplePersistentEnvExtension { addEntryFn := addEntry addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch + asyncMode := .sync } def cacheSpec (key : Expr) (declName : Name) : CoreM Unit :=