feat: split Lean.Kernel.Environment from Lean.Environment

src/CMakeLists.txt

@@ -698,17 +698,17 @@ 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
     VERBATIM)
-  add_custom_target(lake ALL
+  add_custom_target(lake #ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake

src/Lean/AddDecl.lean

@@ -14,15 +14,23 @@ 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
     addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
 
 def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do
+    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := do
   let env ← addDecl env opts decl cancelTk?
   compileDecl env opts decl
 

src/Lean/Compiler/Old.lean

@@ -61,10 +61,10 @@ Compile the given block of mutual declarations.
 Assumes the declarations have already been added to the environment using `addDecl`.
 -/
 @[extern "lean_compile_decls"]
-opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
+opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment
 
 /-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
-def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
+def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except Kernel.Exception Environment :=
   compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
 
 end Environment

src/Lean/CoreM.lean

@@ -523,7 +523,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     return (← getEnv).compileDecl opts decl
   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 =>
@@ -535,7 +535,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
     compileDeclsNew decls
   match (← getEnv).compileDecls 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
   | Declaration.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