You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
Description
In leanprover/lean4:v4.8.0-rc1, with an LSP-aware editor, on opening a file or when imports have changed, for each recursively imported file, the language server sends a textDocument/publishDiagnostics notification with a message of the form "[k/n] Building X.Y.Z", even for files which do not need to be rebuilt.
In previous releases, such notifications are sent only for files which do need to be rebuilt, which has two advantages. Firstly it provides useful information to the user about which files are being built. Secondly there is less work for the client in processing and rendering the message, leading to faster startup.
Context
For a file with import Mathlib, about 4500 diagnostics are sent.
This is new behavior and not very well received, it's a side effect of the new logging architecture but I'm increasingly convinced we need a way to fix it anyway [Mario Carneiro]
Also, it would be nice to have issues for these things, so I can have a recrod of the various improvements people would like to the logging output and keep them in mind [Mac Malone]
Steps to Reproduce
lake +leanprover/lean4:v4.8.0-rc1 new xxx lib
cd xxx
lake build
Open the file "xxx/Xxx.lean" in an LSP-aware editor. Check its JSONRPC event log. There is a textDocument/publishDiagnostics notification with message "[1/1] Building Xxx.Basic\n".
Expected behavior: No such diagnostic is sent, since no file needs to be built
Actual behavior: A diagnostic is sent for every recursive dependency
Versions
Lean (version 4.8.0-rc1, x86_64-w64-windows-gnu, commit dcccfb7, Release)
Windows 10 Pro 22H2 (build 19045.4291)
With #4127, only jobs that do something significant now have a caption printed in non-terminal mode (e.g., the server), So this will hopefully be addressed in RC2.
Prerequisites
Description
In
leanprover/lean4:v4.8.0-rc1
, with an LSP-aware editor, on opening a file or when imports have changed, for each recursively imported file, the language server sends atextDocument/publishDiagnostics
notification with a message of the form "[k/n] Building X.Y.Z", even for files which do not need to be rebuilt.In previous releases, such notifications are sent only for files which do need to be rebuilt, which has two advantages. Firstly it provides useful information to the user about which files are being built. Secondly there is less work for the client in processing and rendering the message, leading to faster startup.
Context
For a file with
import Mathlib
, about 4500 diagnostics are sent.Zulip
Steps to Reproduce
lake +leanprover/lean4:v4.8.0-rc1 new xxx lib
cd xxx
lake build
textDocument/publishDiagnostics
notification with message"[1/1] Building Xxx.Basic\n"
.Expected behavior: No such diagnostic is sent, since no file needs to be built
Actual behavior: A diagnostic is sent for every recursive dependency
Versions
Lean (version 4.8.0-rc1, x86_64-w64-windows-gnu, commit dcccfb7, Release)
Windows 10 Pro 22H2 (build 19045.4291)
Additional Information
Impact
Add 👍 to issues you consider important.
The text was updated successfully, but these errors were encountered: