feat: per-package server options #2456
Conversation
src/Lean/Server/Watchdog.lean
Outdated
| if let some path := fileUriToPath? m.uri then | ||
| if let some (_, pkg) ← searchModuleNameAndPkgOfFileName path st.pkgSearchPath then | ||
| if let some pkgArgs := st.pkgArgs.find? pkg then | ||
| args := pkgArgs |
There was a problem hiding this comment.
A comment explaining why we opt to replace rather than extend the arguments would be nice here; I can potentially see extension being the better option, at least in the context of arguments that wouldn't break compilation.
There was a problem hiding this comment.
Note that in the case that came up on zulip (browsing std from mathlib), the "original" arguments passed to the server are mathlib's and the package arguments are std's (std has no package options), so extending would cause the same issue as already exists.
If we have both global and package-global server arguments, then it would be reasonable to combine the global args with the package-global args for the current package here. But currently there is only one moreServerArgs, and this PR interprets it as package-global.
There was a problem hiding this comment.
@digama0 As I mentioned in the Zulip thread, moreServerArgs is global. moreLeanArgs is the package-specific one. Thus, it should be a combination of the two.
There was a problem hiding this comment.
moreLeanArgs is also documented as only applying to the CLI build though, not the server (and the names back this interpretation up). Nothing about those names suggest that one is global and the other is package-specific, although one of them is on the package and the other is on the library.
Anyway, the current set of options (and the docs on them) is insufficient to cover all the cases, so just spec something out and I'll implement it.
There was a problem hiding this comment.
@digama0 Which brings up another point, it should not just be using the package's moreLeanArgs, but that of the library or executable the module belongs to (and the docs should be updated accordingly). The reason why moreServerArgs is not on those smaller subdivisions is because it is not per-file. Admittedly, it is nowhere noted that moreServerArgs is workspace-global rather than just package-global (except for the the fact they are mentioned to be pass to lean --server, which until this point implied workspace-global), but that is how I think of it. If you think it is worthwhile to separate compilation arguments and server arguments, feel free to add a new moreServerArgs / moreLocalServerArgs field to LeanConfig and/or rename moreServerArgs to moreGlobalServerArgs.
There was a problem hiding this comment.
I implemented moreGlobalServerArgs and added moreServerArgs as indicated. Unfortunately, the implementation is not perfectly accurate because the server does not actually know the precise import structure of each package: if it sees something in the lib's folder then it assumes it is from the lib, even if it is not a transitive import of the root library. This is potentially a problem for packages like mathlib, because there are several libs (e.g. Mathlib, Counterexamples) that share the same root folder (the repo root), because the Mathlib/ folder doesn't count as part of the srcDir and hence there is a lot of overlap between the directory roots for each lib.
As a result per-lib moreServerArgs doesn't really work in mathlib and other projects that have multiple libs with the same root directory. This isn't likely to be an issue for mathlib though since it can just set the moreServerArgs at the package level - it isn't (currently) attempting to set options differently per-lib. If it did want to do so, it would have to put them in separate folders, or we would have to revisit this logic to give the server more project structure information.
There was a problem hiding this comment.
@digama0 Thank you for the changes! 😁 To fix the problem, could you call get-pkg-args (or, I guess get-mod-args) for the file each time before starting a worker to get the arguments of the that module? The would hopefully make per-lib configurations work correctly in all cases. While it may introduce some overhead, restarting a file already takes some time (due to building imports) so I do not think additional overhead would noticeable..
|
Closed in favor of #2858. |
This PR adds per-package server options to resolve #2455. It is based on the previous work in #2456, but takes a different approach: options are loaded for the specific file in the file worker when `print-paths` is called, instead of loading them in the watchdog with a separate Lake command. This change addresses review comments made in #2456. In doing so, it introduces two new Lake config fields: - `leanOptions`: `-D` flag options that are passed to both the language server and `lean` when building. - `moreServerOptions`: `-D` flag options that are passed to the language server. Since `print-paths` must also accept a file path to compute the options for that file, this PR is changing the API for `print-paths`. As there have been numerous complaints about the name `print-paths`, I also decided to change it to `setup-file` in this PR, since it would break compatibility with the old Lake API anyways. This PR deprecates the Lakefile field `moreServerArgs` in favor of `moreGlobalServerArgs`, as suggested in the review for #2456. Fixes #2455 --------- Co-authored-by: digama0 <mcarneir@andrew.cmu.edu>
External Contribution Guidelines.
Proposal implementation of RFC: fixes #2455