Progress notification server protocol extension p. (Pre-RFC)

Stream: lean4

[Gabriel Ebner]

Progress notification server protocol extension proposal (Pre-RFC)

Introduction

The Lean 3 extensions for Emacs and VS Code feature a progress indicator that shows which parts of a file are still being processed by Lean---the "orange bars". This feature is useful because it allows you to tell at a glance whether a definition was accepted without error or is still being elaborated.

In Lean 4, the only progress information available from the server are diagnostics with the message "processing..." (meaning that everything coming after the diagnostic is still being processed). The extension for VS Code parses these messages heuristically and displays orange bars based on these diagnostics.

However, these diagnostics have several shortcomings.

• First of all, parsing the message string is clearly fragile. Any error with the message "processing..." will also cause a progress bar to appear.

• There are also other diagnostic messages which indicate that the server is busy: for example the stderr output of leanpkg print-paths. These are not captured by the string comparison.

• The last point is partly an issue with the current implementation. The "processing..." diagnostics are printed too late, only after a command has been elaborated. This makes it often impossible to tell whether Lean is busy or not.

Proposal

We introduce a new notification, $/lean/fileProgress, containing the ranges that are still being processed. This notification should be sent by the server before processing is started.

interface LeanFileProgressProcessingInfo {
  /** Range which is still being processed */
  range: Range;

  // Further fields may be added in the future.
}

interface LeanFileProgressParams {
  /** The text document to which this progress notification applies. */
  textDocument: TextDocumentIdentifier;

  /**
   * Array containing the parts of the file which are still being processed.
   * The array should be empty if and only if the server is finished processing.
   */
  processing: LeanFileProgressProcessingInfo[];
}

The processing field is an array to allow for future extensibility. At the moment, it will contain either zero or one elements: zero if the server is finished, and one if it is busy.

The "processing..." diagnostic should no longer be sent. Stderr output from leanpkg print-paths would still appear as a diagnostic.

Alternatives

• Send the "processing..." diagnostic earlier and also while leanpkg print-paths is being run. Continue parsing the diagnostics and accept false positive with certain error messages.

• Add an additional non-standard data field to the diagnostics, which indicates that these are progress indicators.

• Send a combined notification for all files, instead of separately.

[Sebastian Ullrich]

SGTM

[Simon Cruanes]

Maybe naive, but there's a relatively new progress feature in LSP. Not sure how VScode displays it.

[Gabriel Ebner]

I've also seen this part of the specification. However I can't even remotely figure out what it's supposed to do from the specification. After studying the vscode-languageserver-node implementation, I believe it is used to show progress bars ("in a generic fashion"??).

Our use case does not seem to be covered by this notification. We want to annotate ranges in a file, not show a progress bar (which the vscode client would show, by interpreting the generic progress info as percentages).

[Marc Huisinga]

I vaguely remember that we would've liked to use the LSP progress feature for requests (specifically: partial result progress), but VSCode did not support it and @Sebastian Ullrich had to hack around it. A quick search through vscode-languageserver-node shows that there seems to be no usage of partial result progress in the client folder. There's also an issue: https://github.com/microsoft/vscode/issues/105870

[Marc Huisinga]

I think it does support "Work Done Progress" (which is used only to display a loading bar or something similar) but as Gabriel says that isn't sufficient for the progress that we'd like in Lean.

[Simon Cruanes]

Ok, that makes sense indeed. I think diagnostics can be abused by sending them many times with changes (like, after parsing, put "processing" on all definitions, and replace them with actual results or remove them as you go), but it's a hack.

[Gabriel Ebner]

Simon Cruanes said:

I think diagnostics can be abused by sending them many times with changes

This is indeed how we used to do it, I've listed a few reasons in the initial post detailing where this falls short.