feat: importModules without loading environment extensions

[Kha]

This PR ensures that environments can be loaded, repeatedly, without executing arbitrary code

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6325 has successfully built against this PR. (2024-12-06 10:36:09) View Log
• 💥 Mathlib branch lean-pr-testing-6325 build failed against this PR. (2024-12-06 13:16:44) View Log
• 💥 Mathlib branch lean-pr-testing-6325 build failed against this PR. (2024-12-09 12:17:29) View Log
• 💥 Mathlib branch lean-pr-testing-6325 build failed against this PR. (2024-12-09 13:24:27) View Log
• ✅ Mathlib branch lean-pr-testing-6325 has successfully built against this PR. (2024-12-09 14:57:05) View Log
• ✅ Mathlib branch lean-pr-testing-6325 has successfully built against this PR. (2024-12-10 11:50:17) View Log
• ✅ Mathlib branch lean-pr-testing-6325 has successfully built against this PR. (2024-12-10 12:33:55) View Log
• ✅ Mathlib branch lean-pr-testing-6325 has successfully built against this PR. (2024-12-10 13:58:24) View Log

[tydeu]

@Kha mkInitialExtensionStates also runs arbitrary I/O. Thus, the entire setup of environment extensions would need to be disabled to avoid this.

Also, what is the reason for privatizing finalizeImport? Downstream users may need to reimplement importModules manually and have it public is key to that. For instance, loading plugins (and then configuring any related settings) needs to be done in the withImporting block.

EDIT: Personally, I would suggest splitting finalizeImport into two separate definitions: importConstants and initializeExtensions.

[Kha]

mkInitialExtensionStates also runs arbitrary I/O

But we're not loading any non-builtin extensions when initializers are disabled, as discussed before.

For instance, loading plugins (and then configuring any related settings) needs to be done in the withImporting block.

So --plugin is broken?

[digama0]

Also, what is the reason for privatizing finalizeImport? Downstream users may need to reimplement importModules manually and have it public is key to that. For instance, loading plugins (and then configuring any related settings) needs to be done in the withImporting block.

Agreed, this would be really annoying. I am calling that function in lean4lean, this will need me to copy paste a lot of code.

[Kha]

I didn't reply to that part because I was already reverting it :)

[tydeu]

@Kha

mkInitialExtensionStates also runs arbitrary I/O

But we're not loading any non-builtin extensions when initializers are disabled, as discussed before.

True, so it is currently safe. It does mean that we have to continually be careful to not introduce any opportunity for arbitrary I/O in a mkInitial going forward. In my opinion, it seems easier (and more principled) to just avoid initializing extensions altogether in sensitive cases (thus avoiding future footguns).

For instance, loading plugins (and then configuring any related settings) needs to be done in the withImporting block.

So --plugin is broken?

Sorry, I should have been more specific. Only loading plugins in Lean code (via Lean.loadPlugin) needs to be done in a withImporting block (to enable Environment-based initializers that require Lean.initializing). --plugin works because it is run during IO.initializing (which also implies Lean.initializing).

[Kha]

@digama0 Actually could you explain what importModulesCore is used for in lean4{lean,checker} that couldn't be done with importModules mod.imports?

[digama0]

I forget all the details, but looking at it now it seems to be a one-step unrolling of importModulesCore #[{module}] . That is, it is creating an environment that uses the target file as its only import, rather than creating an environment prepared for the imports of the target file and doing the target file via the normal elaboration pathway. But for lean4lean I think this is still suboptimal and I want a version of this function that I can prove properties about, so I think (1) importModules mod.imports (loadExts := false) is close enough to what I want for now and (2) eventually this will be replaced by a manual reimplementation that moves everything into pure code so I can prove theorems about it, and the main thing lean core can do to help here is to factor things out into pure and impure parts where sensible (so I eagerly await your Lean.Kernel.Environment PR #5145).

[eric-wieser]

leanprover-community/mathlib4#20355 should stop the bleeding downstream of Mathlib until this lands.