From 89b65c8f1d6fa7700d73f1bc12db0b140c728e32 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 4 Oct 2023 13:02:54 +0200
Subject: [PATCH] feat: make `Environment.mk` private (#2604)

* feat: make `Environment.mk` private

---------
---
 src/Lean/Environment.lean            |  5 ++++-
 tests/lean/prvCtor.lean              |  8 +++++++-
 tests/lean/prvCtor.lean.expected.out | 10 ++++++----
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index a4a9ad16f7..59d0bbbf65 100644
--- a/src/Lean/Environment.lean
+++ b/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 }
 
 /--
diff --git a/tests/lean/prvCtor.lean b/tests/lean/prvCtor.lean
index 18a978732c..28c1bcb2a0 100644
--- a/tests/lean/prvCtor.lean
+++ b/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
 
diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out
index 76f48d8183..f175e7d2fd 100644
--- a/tests/lean/prvCtor.lean.expected.out
+++ b/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'