Skip to content

Commit 2525330

Browse files
Khakim-em
authored andcommitted
fix: make sure all kernel constants are persisted eventually (#8238)
This PR avoids an issue where, through other potential bugs, constants that are tracked by `Kernel.Environment` but not `Environment` are not persisted. (cherry picked from commit af51e3e)
1 parent ffa6cdc commit 2525330

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

src/Lean/Environment.lean

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1663,10 +1663,14 @@ def mkModuleData (env : Environment) (level : OLeanLevel := .private) : IO Modul
16631663
let kenv := env.toKernelEnv
16641664
let env := env.setExporting (level != .private)
16651665
let constNames := kenv.constants.foldStage2 (fun names name _ => names.push name) #[]
1666-
-- not all kernel constants may be exported
1667-
let constants := constNames.filterMap fun n =>
1668-
env.find? n <|>
1669-
guard (looksLikeOldCodegenName n) *> kenv.find? n
1666+
-- not all kernel constants may be exported at `level < .private`
1667+
let constants := if level == .private then
1668+
-- (this branch makes very sure all kernel constants are exported eventually)
1669+
kenv.constants.foldStage2 (fun cs _ c => cs.push c) #[]
1670+
else
1671+
constNames.filterMap fun n =>
1672+
env.find? n <|>
1673+
guard (looksLikeOldCodegenName n) *> kenv.find? n
16701674
let constNames := constants.map (·.name)
16711675
return { env.header with
16721676
extraConstNames := env.checked.get.extraConstNames.toArray

0 commit comments

Comments
 (0)