chore: revise environment constant addition details (#8610)

* Move constant registration with elab env from `Lean.addDecl` to
`Lean.Environment.addDeclCore` for compatibility
* Make module system behavior independent of `Elab.async` value

src/Lean/AddDecl.lean

@@ -84,9 +84,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   -- namespaces
   modifyEnv (decl.getNames.foldl registerNamePrefixes)
 
-  if !Elab.async.get (← getOptions) then
-    return (← addSynchronously)
-
   -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
   -- kernel checking has finished; not all cases are supported yet
   let mut exportedInfo? := none
@@ -106,7 +103,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
         exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
       pure (defn.name, .defnInfo defn, .defn)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
-    | _ => return (← addSynchronously)
+    | _ => return (← doAdd)
 
   if decl.getTopLevelNames.all isPrivateName then
     exportedInfo? := none
@@ -125,30 +122,26 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   -- report preliminary constant info immediately
   async.commitConst async.asyncEnv (some info) (exportedInfo? <|> info)
   setEnv async.mainEnv
-  let cancelTk ← IO.CancelToken.new
-  let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => do
+
+  let doAddAndCommit := do
     setEnv async.asyncEnv
     try
       doAdd
     finally
       async.commitCheckEnv (← getEnv)
-  let t ← BaseIO.mapTask checkAct env.checked
-  let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
-  Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
+
+  if Elab.async.get (← getOptions) then
+    let cancelTk ← IO.CancelToken.new
+    let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => doAddAndCommit
+    let t ← BaseIO.mapTask checkAct env.checked
+    let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
+    Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
+  else
+    try
+      doAddAndCommit
+    finally
+      setEnv async.mainEnv
 where
-  addSynchronously := do
-    doAdd
-    -- make constants known to the elaborator; in the synchronous case, we can simply read them from
-    -- the kernel env
-    for n in decl.getNames do
-      let env ← getEnv
-      let some info := env.checked.get.find? n | unreachable!
-      -- do *not* report extensions in synchronous case at this point as they are usually set only
-      -- after adding the constant itself
-      let res ← env.addConstAsync (reportExts := false) n (.ofConstantInfo info)
-      res.commitConst env (info? := info)
-      res.commitCheckEnv res.asyncEnv
-      setEnv res.mainEnv
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do

src/Lean/Environment.lean

@@ -676,11 +676,31 @@ def addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declarati
     if let some n := decl.getTopLevelNames.find? (!ctx.mayContain ·) then
       throw <| .other s!"cannot add declaration {n} to environment as it is restricted to the \
         prefix {ctx.declPrefix}"
-  if doCheck then
+  let mut env ← if doCheck then
     addDeclCheck env maxHeartbeats decl cancelTk?
   else
     addDeclWithoutChecking env decl
 
+  -- Let the elaborator know about the new constants. This uses the same constant for both
+  -- visibility scopes but the caller can still customize the public one on the main elaboration
+  -- branch by use of `addConstAsync` as is the case for `Lean.addDecl`.
+  for n in decl.getNames do
+    let some info := env.checked.get.find? n | unreachable!
+    env := { env with asyncConstsMap.private := env.asyncConstsMap.private.add {
+      constInfo := .ofConstantInfo info
+      exts? := none
+      consts := .pure <| .mk (α := AsyncConsts) default
+    } }
+    -- TODO
+    if true /- !isPrivateName n-/ then
+      env := { env with asyncConstsMap.public := env.asyncConstsMap.public.add {
+        constInfo := .ofConstantInfo info
+        exts? := none
+        consts := .pure <| .mk (α := AsyncConsts) default
+      } }
+
+  return env
+
 @[inherit_doc Kernel.Environment.constants]
 def constants (env : Environment) : ConstMap :=
   env.toKernelEnv.constants