refactor: move registration of namespaces on kernel add into elaborator

src/Lean/AddDecl.lean

@@ -22,26 +22,55 @@ def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Decl
   else
     addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
 
-def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
+private def Environment.addDeclAux (env : Environment) (opts : Options) (decl : Declaration)
     (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
   if debug.skipKernelTC.get opts then
     addDeclWithoutChecking env decl
   else
     addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
 
+@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
+    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
+  Environment.addDeclAux env opts decl cancelTk?
+
+@[deprecated "use `Lean.addAndCompile`  instead to ensure new namespaces are registered" (since := "2024-12-03")]
 def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
     (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := do
-  let env ← addDecl env opts decl cancelTk?
+  let env ← addDeclAux env opts decl cancelTk?
   compileDecl env opts decl
 
+private def isNamespaceName : Name → Bool
+  | .str .anonymous _ => true
+  | .str p _          => isNamespaceName p
+  | _                 => false
+
+private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
+  match name with
+    | .str _ s =>
+      if s.get 0 == '_' then
+        -- Do not register namespaces that only contain internal declarations.
+        env
+      else
+        go env name
+    | _ => env
+where go env
+  | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
+  | _        => env
+
 def addDecl (decl : Declaration) : CoreM Unit := do
   profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+    let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
         logWarning "declaration uses 'sorry'"
-      match (← getEnv).addDecl (← getOptions) decl (← read).cancelTk? with
-      | .ok    env => setEnv env
-      | .error ex  => throwKernelException ex
+      (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException
+
+    -- 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
+    if let .inductDecl _ _ types _ := decl then
+      env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
+    setEnv env
 
 def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl

src/Lean/Compiler/InitAttr.lean

@@ -144,11 +144,12 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
   let type := mkApp (mkConst `IO) (mkConst `Unit)
   let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
                                      safety := DefinitionSafety.safe }
-  match (← getEnv).addAndCompile {} decl with
-  -- TODO: pretty print error
-  | Except.error e => do
-    let msg ← (e.toMessageData {}).toString
+  try
+    addAndCompile decl
+  catch e => do
+    -- TODO: pretty print error
+    let msg ← e.toMessageData.toString
     throwError "failed to emit registration code for builtin '{forDecl}': {msg}"
-  | Except.ok env  => IO.ofExcept (setBuiltinInitAttr env name) >>= setEnv
+  IO.ofExcept (setBuiltinInitAttr (← getEnv) name) >>= setEnv
 
 end Lean

src/Lean/Elab/BuiltinCommand.lean

@@ -124,9 +124,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
-  | Except.ok env   => setEnv env
-  | Except.error ex => throwError (ex.toMessageData (← getOptions))
+  liftCoreM <| addDecl Declaration.quotDecl
 
 @[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
   let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax

src/Lean/Environment.lean

@@ -1077,34 +1077,9 @@ def isNamespace (env : Environment) (n : Name) : Bool :=
 def getNamespaceSet (env : Environment) : NameSSet :=
   namespacesExt.getState env
 
-private def isNamespaceName : Name → Bool
-  | .str .anonymous _ => true
-  | .str p _          => isNamespaceName p
-  | _                 => false
-
-private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
-  match name with
-    | .str _ s =>
-      if s.get 0 == '_' then
-        -- Do not register namespaces that only contain internal declarations.
-        env
-      else
-        go env name
-    | _ => env
-where go env
-  | .str p _ => if isNamespaceName p then go (registerNamespace env p) p else env
-  | _        => env
-
 @[export lean_elab_environment_update_base_after_kernel_add]
-private def updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (base : Kernel.Environment) : Environment := Id.run do
-  let mut env := { env with base }
-  env := added.getNames.foldl registerNamePrefixes env
-  if let .inductDecl _ _ types _ := added then
-    -- also register inductive type names as namespaces; this used to be done by the kernel itself
-    -- when adding e.g. the recursor but now that the environment extension API exists only for
-    -- `Lean.Environment`, we have to do it here
-    env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
-  env
+private def updateBaseAfterKernelAdd (env : Environment) (base : Kernel.Environment) : Environment :=
+  { env with base }
 
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit := do

src/Lean/ParserCompiler.lean

@@ -103,11 +103,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
           name := c', levelParams := []
           type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe
         }
-        let env ← getEnv
-        let env ← match env.addAndCompile {} decl with
-          | Except.ok    env => pure env
-          | Except.error kex => do throwError (← (kex.toMessageData {}).toString)
-        setEnv <| ctx.combinatorAttr.setDeclFor env c c'
+        addAndCompile decl
+        modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then
           if let some kind ← parserNodeKind? cinfo.value! then
             -- If the parser is parameter-less and produces a node of kind `kind`,

src/Lean/Replay.lean

@@ -55,7 +55,7 @@ def throwKernelException (ex : Kernel.Exception) : M Unit := do
 
 /-- Add a declaration, possibly throwing a `Kernel.Exception`. -/
 def addDecl (d : Declaration) : M Unit := do
-  match (← get).env.addDecl {} d with
+  match (← get).env.addDeclCore 0 d (cancelTk? := none) with
   | .ok env => modify fun s => { s with env := env }
   | .error ex => throwKernelException ex
 

src/library/elab_environment.cpp

@@ -11,19 +11,17 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include "library/compiler/ir_interpreter.h"
 
 namespace lean {
-/* updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (base : Kernel.Environment) :
-   Environment
+/* updateBaseAfterKernelAdd (env : Environment) (base : Kernel.Environment) : Environment
 
-   Updates an elab environment with a given kernel environment after the declaration `d` has been
-   added to it. `d` is used to adjust further elab env data such as registering new namespaces.
+   Updates an elab environment with a given kernel environment.
 
    NOTE: Ideally this language switching would not be necessary and we could do all this in Lean
    only but the old code generator and `mk_projections` still need a C++ `elab_environment::add`. */
-extern "C" obj_res lean_elab_environment_update_base_after_kernel_add(obj_arg env, obj_arg d, obj_arg kenv);
+extern "C" obj_res lean_elab_environment_update_base_after_kernel_add(obj_arg env, obj_arg kenv);
 
 elab_environment elab_environment::add(declaration const & d, bool check) const {
     environment kenv = to_kernel_env().add(d, check);
-    return elab_environment(lean_elab_environment_update_base_after_kernel_add(this->to_obj_arg(), d.to_obj_arg(), kenv.to_obj_arg()));
+    return elab_environment(lean_elab_environment_update_base_after_kernel_add(this->to_obj_arg(), kenv.to_obj_arg()));
 }
 
 extern "C" LEAN_EXPORT object * lean_elab_add_decl(object * env, size_t max_heartbeat, object * decl,