chore: clean up after update-stage0

src/CMakeLists.txt

@@ -705,7 +705,7 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     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

@@ -8,27 +8,6 @@ import Lean.CoreM
 
 namespace Lean
 
-register_builtin_option debug.skipKernelTC : Bool := {
-  defValue := false
-  group    := "debug"
-  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 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 Kernel.Exception Environment := do
   let env ← addDecl env opts decl cancelTk?

src/Lean/CoreM.lean

@@ -25,11 +25,6 @@ register_builtin_option diagnostics.threshold : Nat := {
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
 }
 
-register_builtin_option maxHeartbeats : Nat := {
-  defValue := 200000
-  descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
-}
-
 /--
 If the `diagnostics` option is not already set, gives a message explaining this option.
 Begins with a `\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
@@ -45,9 +40,6 @@ namespace Core
 
 builtin_initialize registerTraceClass `Kernel
 
-def getMaxHeartbeats (opts : Options) : Nat :=
-  maxHeartbeats.get opts * 1000
-
 abbrev InstantiateLevelCache := PersistentHashMap Name (List Level × Expr)
 
 /-- Cache for the `CoreM` monad -/

src/Lean/Environment.lean

@@ -101,6 +101,20 @@ structure EnvironmentHeader where
   moduleData   : Array ModuleData := #[]
   deriving Nonempty
 
+register_builtin_option debug.skipKernelTC : Bool := {
+  defValue := false
+  group    := "debug"
+  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"
+}
+
+register_builtin_option maxHeartbeats : Nat := {
+  defValue := 200000
+  descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
+}
+
+def Core.getMaxHeartbeats (opts : Options) : Nat :=
+  maxHeartbeats.get opts * 1000
+
 namespace Kernel
 
 structure Diagnostics where
@@ -161,7 +175,7 @@ structure Environment where
   the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
   Only the code generator uses them.
   -/
-  private const2ModIdx    : Std.HashMap Name ModuleIdx
+  const2ModIdx            : Std.HashMap Name ModuleIdx
   /--
   Environment extensions. It also includes user-defined extensions.
   -/
@@ -226,15 +240,16 @@ and the kernel will not catch it if the new option is set to true.
 @[extern "lean_add_decl_without_checking"]
 opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Exception Environment
 
-/--
-Adds constant to the environment without type checking it.
+/-- Add given declaration to the environment, respecting `debug.skipKernelTC`. -/
+def 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?
 
-**WARNING** This function is meant for special metaprogramming uses such as in lakefile loading.
-It compromises soundness because, for example, a buggy metaprogram may produce an invalid theorem,
-and the kernel will not catch it if it was added to the environment directly via `add`.
--/
 @[export lean_environment_add]
-def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
+private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
   { env with constants := env.constants.insert cinfo.name cinfo }
 
 @[export lean_kernel_diag_is_enabled]
@@ -297,12 +312,31 @@ def ofKernelEnv (env : Kernel.Environment) : Environment :=
 def toKernelEnv (env : Environment) : Kernel.Environment :=
   env.base
 
+/-- Type check given declaration and add it to the environment. -/
+@[extern "lean_elab_add_decl"]
+opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
+  (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment
+
+@[inherit_doc Kernel.Environment.addDeclWithoutChecking, extern "lean_elab_add_decl_without_checking"]
+opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Kernel.Exception Environment
+
+def addDecl (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?
+
 @[inherit_doc Kernel.Environment.constants]
 def constants (env : Environment) : ConstMap :=
   env.toKernelEnv.constants
 
-@[inherit_doc Kernel.Environment.add]
-def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
+@[inherit_doc Kernel.Environment.const2ModIdx]
+def const2ModIdx (env : Environment) : Std.HashMap Name ModuleIdx :=
+  env.toKernelEnv.const2ModIdx
+
+@[export lean_elab_environment_add]
+private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
   { env with base := env.base.add cinfo }
 
 /--
@@ -1098,14 +1132,6 @@ private def updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (
     env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
   env
 
-/-- Type check given declaration and add it to the environment. -/
-@[extern "lean_elab_add_decl"]
-opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
-  (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment
-
-@[inherit_doc Kernel.Environment.addDeclWithoutChecking, extern "lean_elab_add_decl_without_checking"]
-opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Kernel.Exception Environment
-
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit := do
   let pExtDescrs ← persistentEnvExtensionsRef.get

src/lake/Lake/Load/Lean/Elab.lean

@@ -79,6 +79,13 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
   else
     return s.commandState.env
 
+/--
+`Lean.Environment.add` is now private, but exported as `lean_elab_environment_add`.
+We call it here via `@[extern]` with a mock implementation.
+-/
+@[extern "lean_elab_environment_add"]
+private opaque addToEnv (env : Environment) (_ : ConstantInfo) : Environment
+
 /--
 Import a configuration `.olean` (e.g., `lakefile.olean`).
 Auxiliary definition for `importConfigFile`.
@@ -98,7 +105,7 @@ def importConfigFileCore (olean : FilePath) (leanOpts : Options) : IO Environmen
   let (mod, _) ← readModuleData olean
   let env ← importModulesUsingCache mod.imports leanOpts 1024
   -- Apply constants (does not go through the kernel, so order is irrelevant)
-  let env := unsafe mod.constants.foldl (·.add) env
+  let env := mod.constants.foldl addToEnv env
   /-
   Below, we pass module environment extension entries to
   `PersistentEnvExtension.addEntryFn` - but for an extension of

tests/lean/prvCtor.lean

@@ -22,7 +22,7 @@ open Lean in
 open Lean in
 #eval id (α := CoreM Unit) do
   -- this implementation is no longer allowed because of a private constructor
-  modifyEnv fun env => { env with header.mainModule := `foo }
+  modifyEnv fun env => { env with base.header.mainModule := `foo }
 
 #check a -- Error
 

tests/lean/prvCtor.lean.expected.out

@@ -1,5 +1,5 @@
 a : Nat
-prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private
+prvCtor.lean:25:23-25:66: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private
 prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize

tests/lean/run/structure.lean

@@ -24,7 +24,7 @@ inductive D
   | mk (x y z : Nat) : D
 
 /--
-info: #[base, const2ModIdx, extensions, extraConstNames, header]
+info: #[constants, quotInit, diagnostics, const2ModIdx, extensions, extraConstNames, header]
 #[toS2, toS1, x, y, z, toS3, w, s]
 (some [S4.toS2, S2.toS1])
 #[S2, S3]
@@ -33,7 +33,7 @@ info: #[base, const2ModIdx, extensions, extraConstNames, header]
 #guard_msgs in
 #eval show CoreM Unit from do
   let env ← getEnv
-  IO.println (getStructureFields env `Lean.Environment)
+  IO.println (getStructureFields env ``Kernel.Environment)
   check $ getStructureFields env `S4 == #[`toS2, `toS3, `s]
   check $ getStructureFields env `S1 == #[`x, `y]
   check $ isSubobjectField? env `S4 `toS2 == some `S2