feat: importModules without loading environment extensions#6325
feat: importModules without loading environment extensions#6325kim-em merged 2 commits intoleanprover:masterfrom
importModules without loading environment extensions#6325Conversation
|
Mathlib CI status (docs):
|
570f669 to
81447dd
Compare
|
@Kha Also, what is the reason for privatizing EDIT: Personally, I would suggest splitting |
But we're not loading any non-builtin extensions when initializers are disabled, as discussed before.
So |
Agreed, this would be really annoying. I am calling that function in lean4lean, this will need me to copy paste a lot of code. |
81447dd to
0c4532f
Compare
|
I didn't reply to that part because I was already reverting it :) |
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
Sorry, I should have been more specific. Only loading plugins in Lean code (via |
|
@digama0 Actually could you explain what |
0c4532f to
542c80d
Compare
cb6d977 to
8e6f0cc
Compare
|
I forget all the details, but looking at it now it seems to be a one-step unrolling of |
|
leanprover-community/mathlib4#20355 should stop the bleeding downstream of Mathlib until this lands. |
These are not supported unless `enableInitializersExecution` is called, and various downstream scripts do not call this. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/lean4checker.20failure/near/486191171 has some context for the underlying issue, which seems to be that Lean tries to finalize environment extensions even if initializers are disabled, leading to crashes if those extensions (such as the parser alias table) expect initializers to have run. To prove this works, this removes `Lean.enableInitializersExecution` from the script to check the yaml files. This is what we will want to do anyway after leanprover/lean4#6325 lands, as this script should not need to run any extensions.
This PR ensures that environments can be loaded, repeatedly, without executing arbitrary code (cherry picked from commit 5df4e48)
This PR ensures that environments can be loaded, repeatedly, without executing arbitrary code (cherry picked from commit 5df4e48)
… correctly (#29513) Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](leanprover/lean4#6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
The `overwrite_index.lean` script failed to count attributes after a Lean version bump. This was due to changes in how module imports handle environment extensions, as introduced in leanprover/lean4#6325 . `Lean.withImportModules` no longer loads environment extensions. This commit refactors the `runWithImports` function to use the lower-level `importModulesCore` and `finalizeImport` functions, explicitly setting `loadExts := true` to ensure attributes are loaded and counted correctly.
… correctly (leanprover-community#29513) Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](leanprover/lean4#6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
The `releases_drafts/` folder contained two entries that were already covered in earlier releases: - `module-system.md` — the module system was stabilized in v4.27.0 (#11637) - `environment.md` — the `importModules`/`finalizeImport` `loadExts` change landed in v4.20.0 (#6325) Discovered while preparing the v4.29.0-rc1 release notes. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ensures that environments can be loaded, repeatedly, without executing arbitrary code