Skip to content

Commit

Permalink
fix: make several LCNF environment extensions have asyncMode of .sync (
Browse files Browse the repository at this point in the history
…#7041)

This PR marks several LCNF-specific environment extensions as having an
asyncMode of .sync rather than the default of .mainOnly, so they work
correctly even in async contexts.
  • Loading branch information
zwarich authored Feb 12, 2025
1 parent cc04b04 commit 9dfe570
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/Lean/Compiler/LCNF/Passes.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down
1 change: 1 addition & 0 deletions src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/Lean/Compiler/LCNF/SpecInfo.lean
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
addEntryFn := SpecState.addEntry
addImportedFn := fun _ => {}
toArrayFn := fun s => sortEntries s.toArray
asyncMode := .sync
}

/--
Expand Down
1 change: 1 addition & 0 deletions src/Lean/Compiler/LCNF/Specialize.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down

0 comments on commit 9dfe570

Please sign in to comment.