Progress notification server protocol extension proposal

[gebner]

As per the revised contribution guidelines, I am filing an RFC issue in advance of submitting a PR. This RFC has been discussed on Zulip, with unanimously positive feedback.

Progress notification server protocol extension proposal

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: VersionedTextDocumentIdentifier;

  /**
   * 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.

[Kha]

LGTM, please go ahead