feat: make Environment.mk private (#2604)

* feat: make `Environment.mk` private

---------

src/Lean/Environment.lean

@@ -117,6 +117,9 @@ declared by users are stored in an environment extension. Users can declare new
 using meta-programming.
 -/
 structure Environment where
+  /-- The constructor of `Environment` is private to protect against modification
+  that bypasses the kernel. -/
+  private mk ::
   /--
   Mapping from constant name to module (index) where constant has been declared.
   Recall that a Lean file has a header where previously compiled modules can be imported.
@@ -149,7 +152,7 @@ structure Environment where
 
 namespace Environment
 
-def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
+private def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
   { env with constants := env.constants.insert cinfo.name cinfo }
 
 /--

tests/lean/prvCtor.lean

@@ -16,7 +16,13 @@ def n2 : Name "hello" := ⟨"hello"⟩
 def n3 : Name "hello" := Name.mk "hello"
 
 open Lean in
-#eval id (α := CoreM Unit) do modifyEnv fun env => { env with header.mainModule := `foo } -- change module name to test `private`
+#eval id (α := CoreM Unit) do
+  modifyEnv fun env => env.setMainModule `foo -- change module name to test `private`
+
+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 }
 
 #check a -- Error
 

tests/lean/prvCtor.lean.expected.out

@@ -1,10 +1,12 @@
 a : Nat
 
-prvCtor.lean:21:7-21:8: error: unknown identifier 'a'
-prvCtor.lean:23:25-23:27: error: overloaded, errors 
+prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private
+prvCtor.lean:23:0-25:61: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
+prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize instance
     EmptyCollection (Name "hello")
   
   invalid {...} notation, constructor for `Name` is marked as private
-prvCtor.lean:25:25-25:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private
-prvCtor.lean:27:25-27:40: error: unknown constant 'Name.mk'
+prvCtor.lean:31:25-31:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private
+prvCtor.lean:33:25-33:40: error: unknown constant 'Name.mk'