leanprover/lean4

'Building X' diagnostic for every dependency when processing imports

Closed this issue · 2 comments

bustercopley commented

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • 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.

Zulip

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

  1. lake +leanprover/lean4:v4.8.0-rc1 new xxx lib
  2. cd xxx
  3. lake build
  4. 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)

Additional Information

Impact

Add 👍 to issues you consider important.

semorrison commented

When we have a fix, let's backport to rc2.

tydeu commented

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.