Skip to content

Commit

Permalink
chore: don't forget about namespace reservation for async-unsupported…
Browse files Browse the repository at this point in the history
… constant kinds
  • Loading branch information
Kha committed Feb 7, 2025
1 parent 1248a55 commit 4b30849
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions src/Lean/AddDecl.lean
Original file line number Diff line number Diff line change
Expand Up @@ -50,15 +50,13 @@ where go env
| _ => env

def addDecl (decl : Declaration) : CoreM Unit := do
let mut env ← getEnv
-- register namespaces for newly added constants; this used to be done by the kernel itself
-- but that is incompatible with moving it to a separate task
env := decl.getNames.foldl registerNamePrefixes env
modifyEnv (decl.getNames.foldl registerNamePrefixes)
if let .inductDecl _ _ types _ := decl then
env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
modifyEnv (types.foldl (registerNamePrefixes · <| ·.name ++ `rec))

if !Elab.async.get (← getOptions) then
setEnv env
return (← doAdd)

-- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
Expand All @@ -70,6 +68,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
| .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
| _ => return (← doAdd)

let env ← getEnv
-- no environment extension changes to report after kernel checking; ensures we do not
-- accidentally wait for this snapshot when querying extension states
let async ← env.addConstAsync (reportExts := false) name kind
Expand Down

0 comments on commit 4b30849

Please sign in to comment.