refactor: move registration of namespaces on kernel add into elaborator

Author: Kha

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/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/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,