feat: server support for new module setup #8699
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mhuisi
reviewed
Jun 10, 2025
|
!bench |
|
Here are the benchmark results for commit 27b9014. Benchmark Metric Change
==============================================
+ bv_decide_mod task-clock -2.1% (-31.8 σ)
+ bv_decide_mod wall-clock -2.2% (-206.6 σ)
- rbmap_library task-clock 6.9% (44.1 σ)
- rbmap_library wall-clock 6.9% (36.0 σ) |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 18, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 18, 2025
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 19, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 19, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 19, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 19, 2025
mhuisi
reviewed
Jun 23, 2025
This reverts commit e0e3c0e.
mhuisi
approved these changes
Jun 23, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 23, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 23, 2025
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
This PR adds support to the server for the new module setup process by changing how `lake setup-file` is used. In the new server setup, `lake setup-file` is invoked with the file name of the edited module passed as a CLI argument and with the parsed header passed to standard input in JSON form. Standard input is used to avoid potentially exceeding the CLI length limits on Windows. Lake will build the module's imports along with any other dependencies and then return the module's workspace configuration via JSON (now in the form of `ModuleSetup`). The server then post-processes this configuration a bit and returns it back to the Lean language processor. The server's header is currently only fully respected by Lake for external modules (files that are not part of any workspace library). For workspace modules, the saved module header is currently used to build imports (as has been done since leanprover#7909). A follow-up Lake PR will align both cases to follow the server's header. Lean search paths (e.g., `LEAN_PATH`, `LEAN_SRC_PATH`) are no longer negotiated between the server and Lake. These environment variables are already configured during sever setup by `lake serve` and do not change on a per-file basis. Lake can also pre-resolve the `.olean` files of imports via the `importArts` field of `ModuleSetup`, limiting the potential utility of communicating `LEAN_PATH`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support to the server for the new module setup process by changing how
lake setup-fileis used.In the new server setup,
lake setup-fileis invoked with the file name of the edited module passed as a CLI argument and with the parsed header passed to standard input in JSON form. Standard input is used to avoid potentially exceeding the CLI length limits on Windows. Lake will build the module's imports along with any other dependencies and then return the module's workspace configuration via JSON (now in the form ofModuleSetup). The server then post-processes this configuration a bit and returns it back to the Lean language processor.The server's header is currently only fully respected by Lake for external modules (files that are not part of any workspace library). For workspace modules, the saved module header is currently used to build imports (as has been done since #7909). A follow-up Lake PR will align both cases to follow the server's header.
Lean search paths (e.g.,
LEAN_PATH,LEAN_SRC_PATH) are no longer negotiated between the server and Lake. These environment variables are already configured during sever setup bylake serveand do not change on a per-file basis. Lake can also pre-resolve the.oleanfiles of imports via theimportArtsfield ofModuleSetup, limiting the potential utility of communicatingLEAN_PATH.