Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: don't forget about namespace reservation for async-unsupported constant kinds #6987

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore: don't forget about namespace reservation for async-unsupported constant kinds #6987

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions src/Lean/AddDecl.lean
View file
Open in desktop
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
Loading