feat: split Lean.Kernel.Environment from Lean.Environment (#5145)

This PR splits the environment used by the kernel from that used by the
elaborator, providing the foundation for tracking of asynchronously
elaborated declarations, which will exist as a concept only in the
latter.

Minor changes:
* kernel diagnostics are moved from an environment extension to a direct
environment as they are the only extension used directly by the kernel
* `initQuot` is moved from an environment header field to a direct
environment as it is the only header field used by the kernel; this also
makes the remaining header immutable after import

src/CMakeLists.txt

@@ -699,12 +699,12 @@ else()
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_custom_target(lake_lib ALL
+  add_custom_target(lake_lib
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
     VERBATIM)
-  add_custom_target(lake_shared ALL
+  add_custom_target(lake_shared
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS lake_lib
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared

src/Lean/AddDecl.lean

@@ -14,8 +14,16 @@ register_builtin_option debug.skipKernelTC : Bool := {
   descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
 }
 
+/-- Adds given declaration to the environment, respecting `debug.skipKernelTC`. -/
+def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
+    (cancelTk? : Option IO.CancelToken := none) : Except Exception Environment :=
+  if debug.skipKernelTC.get opts then
+    addDeclWithoutChecking env decl
+  else
+    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
+
 def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment :=
+    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
   if debug.skipKernelTC.get opts then
     addDeclWithoutChecking env decl
   else

src/Lean/CoreM.lean

@@ -515,7 +515,7 @@ register_builtin_option compiler.enableNew : Bool := {
 opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 
 @[extern "lean_compile_decls"]
-opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
+opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment
 
 def compileDecl (decl : Declaration) : CoreM Unit := do
   let opts ← getOptions
@@ -526,7 +526,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     return compileDeclsOld (← getEnv) opts decls
   match res with
   | Except.ok env => setEnv env
-  | Except.error (KernelException.other msg) =>
+  | Except.error (.other msg) =>
     checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
     throwError msg
   | Except.error ex =>
@@ -538,7 +538,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
     compileDeclsNew decls
   match compileDeclsOld (← getEnv) opts decls with
   | Except.ok env   => setEnv env
-  | Except.error (KernelException.other msg) =>
+  | Except.error (.other msg) =>
     throwError msg
   | Except.error ex =>
     throwKernelException ex

src/Lean/Declaration.lean

@@ -193,6 +193,19 @@ def Declaration.definitionVal! : Declaration → DefinitionVal
   | .defnDecl val => val
   | _ => panic! "Expected a `Declaration.defnDecl`."
 
+/--
+Returns all top-level names to be defined by adding this declaration to the environment. This does
+not include auxiliary definitions such as projections.
+-/
+def Declaration.getNames : Declaration → List Name
+  | .axiomDecl val          => [val.name]
+  | .defnDecl val           => [val.name]
+  | .thmDecl val            => [val.name]
+  | .opaqueDecl val         => [val.name]
+  | .quotDecl               => [``Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind]
+  | .mutualDefnDecl defns   => defns.map (·.name)
+  | .inductDecl _ _ types _ => types.map (·.name)
+
 @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
   match d with
   | .quotDecl                                        => pure a

src/Lean/Elab/Structure.lean

@@ -681,7 +681,7 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF
       throwErrorAt info.ref msg
 
 @[extern "lean_mk_projections"]
-private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment
+private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except Kernel.Exception Environment
 
 private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
   if r.type.isProp then