feat: make Environment.mk private

[digama0]

As one follow-up to the discussion here and here, one easy way to make it harder for tactic-writers to accidentally modify the environment to add unchecked constants is to make the constructor private.

Against my expectations, this broke literally nothing in lean itself, and only one test (which ironically was testing private constructors); this was switched to use the API function and everything else worked. We'll see what the mathlib breakage is.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2604 has successfully built against this PR. (2023-09-30 02:53:31) View Log
• 💥 Mathlib branch lean-pr-testing-2604 build failed against this PR. (2023-10-03 02:54:35) View Log
• ❌ Mathlib branch lean-pr-testing-2604 built against this PR, but testing failed. (2023-10-03 06:30:35) View Log
• ❌ Mathlib branch lean-pr-testing-2604 built against this PR, but testing failed. (2023-10-04 00:53:23) View Log

[SchrodingerZhu]

How can I obtain an empty Environment for mock testing?

[kim-em]

How can I obtain an empty Environment for mock testing?

Would using Environment.mk via open private from Std suffice for your use case?

[SchrodingerZhu]

How can I obtain an empty Environment for mock testing?

Would using Environment.mk via open private from Std suffice for your use case?

Interesting, just learned that private is not definite Lean.

[kim-em]

How can I obtain an empty Environment for mock testing?

@SchrodingerZhu, sorry, I gave you the wrong answer previously: you can use Lean.mkEmptyEnvironment.

[kim-em]

Making Environment.add private is more complicated: it currently breaks Aesop, but if fixable by using the "replay" functionality of lean4checker directly.

In order to keep things moving, I'm now going to revert the commit to this PR in which I made Environment.add private --- we'll do that later.

[kim-em]

@digama0, if you're happy with my proposed change to the comment, I can merge this.

[digama0]

Hm, the Environment.add part was a mistake, it should be private as well. Can we go forward with the change and calling it via extern as you did? (It would be good if extern was flagged a bit more clearly as unsafe, but it seems visible enough for review purposes. Is there a reason the same technique doesn't work for Aesop?)

[Kha]

Is there a reason the same technique doesn't work for Aesop?

The interpreter only knows how to handle [extern] from compiled modules

[kim-em]

My suggestion is that we merge as is, and then when #2617 is merged Aesop can use that, and then we can make Environment.add private as well.