[fleche] Implement fileProgress notification for document progress

This is modelled after Lean's `$/lean/fileProgress` notification: a yellow bar in the right side panel indicates what parts of the document are still not checked. Fixes #54 TODO / comments: - fix editor selection logic for applying the decorations - we send on fileProgress per sentence, that's likely too much.
ejgallego · Dec 22, 2022 · 5f6f3dd · 5f6f3dd
1 parent fb284e5
commit 5f6f3dd
Show file tree

Hide file tree

Showing 19 changed files with 303 additions and 35 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -13,6 +13,9 @@
  - Improved syntax highlighting on VSCode client (@artagnon, #105)
  - Resume document checking from the point it was interrupted
    (@ejgallego, #95, #99)
+ - Send `$/coq/fileProgress` progress notifications from server,
+   similarly to what Lean does; display them in Code's right gutter
+   (@ejgallego, #106, fixes #54)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

diff --git a/README.md b/README.md
@@ -150,6 +150,12 @@ Supporting inlays and Lean-style info view.
 
 ### Suggestions / Search panel
 
+## Protocol Notes
+
+`coq-lsp` mostly implements the [LSP Standard](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/), plus some extensions specific to Coq.
+
+Check [the `coq-lsp` protocol documentation](etc/doc/PROTOCOL.md) for more details.
+
 ## Development / Building from sources
 
 ### Server:

diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
@@ -138,6 +138,21 @@ let lsp_of_diags ~uri ~version diags =
     diags
   |> LSP.mk_diagnostics ~uri ~version
 
+let lsp_of_progress ~uri ~version progress =
+  let progress =
+    List.map
+      (fun (range, kind) ->
+        `Assoc [ ("range", LSP.mk_range range); ("kind", `Int kind) ])
+      progress
+  in
+  let params =
+    [ ( "textDocument"
+      , `Assoc [ ("uri", `String uri); ("version", `Int version) ] )
+    ; ("processing", `List progress)
+    ]
+  in
+  LSP.mk_notification ~method_:"$/coq/fileProgress" ~params
+
 module Check = struct
   let pending = ref None
 
@@ -151,7 +166,9 @@ module Check = struct
 
   let completed uri =
     let doc = Hashtbl.find doc_table uri in
-    doc.completed = Yes
+    match doc.completed with
+    | Yes _ -> true
+    | _ -> false
 
   let schedule ~uri = pending := Some uri
 end
@@ -179,7 +196,8 @@ let do_change params =
   let uri, version =
     (string_field "uri" document, int_field "version" document)
   in
-  Log.log_error "checking file" (uri ^ " / version: " ^ string_of_int version);
+  (* Log.log_error "checking file" (uri ^ " / version: " ^ string_of_int
+     version); *)
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
   | [] -> ()
@@ -188,12 +206,18 @@ let do_change params =
       "more than one change unsupported due to sync method";
     assert false
   | change :: _ ->
-    let text = string_field "text" change in
+    let contents = string_field "text" change in
     let doc = Hashtbl.find doc_table uri in
     let doc =
       (* [bump_version] will clean stale info about the document, in particular
          partial results of a previous checking *)
-      if version > doc.version then Fleche.Doc.bump_version ~version ~text doc
+      if version > doc.version then (
+        Log.log_error "bump file" (uri ^ " / version: " ^ string_of_int version);
+        let tb = Unix.gettimeofday () in
+        let doc = Fleche.Doc.bump_version ~version ~contents doc in
+        let diff = Unix.gettimeofday () -. tb in
+        Log.log_error "bump file took" (Format.asprintf "%f" diff);
+        doc)
       else doc
     in
     let () = Hashtbl.replace doc_table uri doc in
@@ -347,6 +371,8 @@ let memo_read_from_disk () = if false then memo_read_from_disk ()
 let request_queue = Queue.create ()
 
 let process_input (com : J.t) =
+  if Fleche.Debug.sched_wakeup then
+    Log.log_error "-> enqueue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
   (* TODO: this is the place to cancel pending requests that are invalid, and in
      general, to perform queue optimizations *)
   Queue.push com request_queue;
@@ -397,6 +423,8 @@ let dispatch_message ofmt ~state dict =
     Log.log_error "BT" bt
 
 let rec process_queue ofmt ~state =
+  if Fleche.Debug.sched_wakeup then
+    Log.log_error "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
   (match Queue.peek_opt request_queue with
   | None -> (
     match !Check.pending with
@@ -424,6 +452,9 @@ let lsp_cb oc =
     ; send_diagnostics =
         (fun ~uri ~version diags ->
           lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc)
+    ; send_fileProgress =
+        (fun ~uri ~version progress ->
+          lsp_of_progress ~uri ~version progress |> Lsp.Io.send_json oc)
     }
 
 let lvl_to_severity (lvl : Feedback.level) =

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -5,13 +5,17 @@ import {
     workspace,
     ViewColumn,
     Uri,
+    OverviewRulerLane
 } from "vscode";
-import {
+import * as vscode from "vscode";
+import { Range } from "vscode-languageclient";
+import { 
     LanguageClient,
     LanguageClientOptions,
     RevealOutputChannelOn,
 } from "vscode-languageclient/node";
 import { GoalPanel } from "./goals";
+import { coqFileProgress, CoqFileProgressParams } from "./progress";
 
 let client: LanguageClient;
 let goalPanel: GoalPanel | null;
@@ -40,7 +44,7 @@ export function activate(context: ExtensionContext): void {
             if (goalPanel) goalPanel.dispose();
         }
 
-        window.showInformationMessage("Going to start!");
+        window.showInformationMessage("Coq Language Server: starting");
 
         const config = workspace.getConfiguration("coq-lsp");
         const initializationOptions = {
@@ -64,10 +68,23 @@ export function activate(context: ExtensionContext): void {
         );
         client.start();
 
+        client.onNotification(coqFileProgress, (params) => {
+            let ranges = params.processing.map((fp) => rangeProto2Code(fp.range))
+                                          .filter((r) => ! r.isEmpty);
+            // FIXME (updates the activeTextEditor which doesn't really work)
+            window.activeTextEditor?.setDecorations(progressDecoration, ranges);
+        });
+
         // XXX: Fix this mess with the lifetime of the panel
         goalPanel = panelFactory(context);
     };
+    const progressDecoration = window.createTextEditorDecorationType(
+        { overviewRulerColor: 'rgba(255,165,0,0.5)', overviewRulerLane: OverviewRulerLane.Left}
+    );
 
+    const rangeProto2Code = function(r : Range) {
+        return new vscode.Range(r.start.line, r.start.character, r.end.line, r.end.character);
+    };
     const checkPanelAlive = () => {
         if (!goalPanel) {
             goalPanel = panelFactory(context);

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
@@ -10,6 +10,7 @@ interface Goal {
     ty: string;
     hyps: Hyp[];
 }
+
 interface GoalRequest {}
 
 // returns the HTML code of goals environment

diff --git a/editor/code/src/progress.ts b/editor/code/src/progress.ts
@@ -0,0 +1,26 @@
+import { NotificationType, NotificationType1, VersionedTextDocumentIdentifier, Range } from "vscode-languageclient";
+
+enum CoqFileProgressKind {
+    Processing = 1,
+    FatalError = 2
+}
+
+interface CoqFileProgressProcessingInfo {
+    /** Range for which the processing info was reported. */
+    range: Range;
+    /** Kind of progress that was reported. */
+    kind?: CoqFileProgressKind;
+}
+
+export interface CoqFileProgressParams {
+    /** 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: CoqFileProgressProcessingInfo[];
+}
+
+export const coqFileProgress = new NotificationType<CoqFileProgressParams>('$/coq/fileProgress');
diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
@@ -0,0 +1,125 @@
+# coq-lsp protocol documentation
+
+## Introduction and preliminaries
+
+`coq-lsp` should be usable by standard LSP clients, however it
+implements some extensions tailored to improve Coq-specific use.
+
+As of today, this document is written for the 3.17 version of the LSP specification:
+https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification
+
+See also the upstream LSP issue on generic support for Proof
+Assistants
+https://github.com/microsoft/language-server-protocol/issues/1414
+
+## Language server protocol support table
+
+If a feature doesn't appear here it usually means it is not planned in the short term:
+
+| Method                            | Support | Notes                                                      |
+|-----------------------------------|---------|------------------------------------------------------------|
+| `initialize`                      | Partial | We don't obey the advertised client capabilities           |
+| `client/registerCapability`       | No      | Not planned ATM                                            |
+| `$/setTrace`                      | No      | Planned                                                    |
+| `$/logTrace`                      | No      |                                                            |
+| `window/logMessage`               | Yes     |                                                            |
+|-----------------------------------|---------|------------------------------------------------------------|
+| `textDocument/didOpen`            | Yes     | We can't reuse Memo tables yet                             |
+| `textDocument/didChange`          | Yes     | We only support `TextDocumentSyncKind.Full` for now        |
+| `textDocument/didClose`           | Partial | We'd likely want to save a `.vo` file on close if possible |
+| `textDocument/didSave`            | No      |                                                            |
+|-----------------------------------|---------|------------------------------------------------------------|
+| `notebookDocument/didOpen`        | No      | Planned                                                    |
+|-----------------------------------|---------|------------------------------------------------------------|
+| `textDocument/declaration`        | No      | Planned, blocked on upstream issues                        |
+| `textDocument/definition`         | No      | Planned, blocked on upstream issues (#53)                  |
+| `textDocument/references`         | No      | Planned, blocked on upstream issues                        |
+| `textDocument/hover`              | Yes     |                                                            |
+| `textDocument/codeLens`           | No      |                                                            |
+| `textDocument/foldingRange`       | No      |                                                            |
+| `textDocument/documentSymbol`     | Yes     | Needs more work as to provide better results               |
+| `textDocument/semanticTokens`     | No      | Planned                                                    |
+| `textDocument/inlineValue`        | No      | Planned                                                    |
+| `textDocument/inlayHint`          | No      | Planned                                                    |
+| `textDocument/completion`         | Partial | Needs more work locally and upstream (#50)                 |
+| `textDocument/publishDiagnostics` | Yes     |                                                            |
+| `textDocument/diagnostic`         | No      | Planned, issue #49                                         |
+| `textDocument/codeAction`         | No      | Planned                                                    |
+|-----------------------------------|---------|------------------------------------------------------------|
+| `workspace/workspaceFolders`      | No      |                                                            |
+|-----------------------------------|---------|------------------------------------------------------------|
+
+
+## Extensions to the LSP specification
+
+As of today, `coq-lsp` implements two extensions to the LSP spec. Note
+that none of them are stable yet:
+
+### Goal Display
+
+In order to display proof goals, `coq-lsp` supports the `proof/goals` request, parameters are:
+```typescript
+{ textDocument: uri
+, position: Position
+}
+```
+
+Answer to the request is a `Goal[]` object, where
+```typescript
+interface Hyp {
+    names: string;
+    ty: string;
+}
+interface Goal {
+    ty: string;
+    hyps: Hyp[];
+}
+
+interface CoqFileProgressParams {
+
+```
+
+which can be then rendered by the client in way that is desired.
+
+`proof/goals` was first used in the lambdapi-lsp server implementation, and we adapted it.
+
+#### Changelog
+
+- v1: initial version, imported from lambdapi-lsp
+
+### File checking progress
+
+The `$/coq/fileProgress` notification is sent from server to client to
+describe the ranges of the document that have been processed.
+
+It is modelled after `$/lean/fileProgress`, see
+https://github.com/microsoft/language-server-protocol/issues/1414 for more information.
+
+```typescript
+enum CoqFileProgressKind {
+    Processing = 1,
+    FatalError = 2
+}
+
+interface CoqFileProgressProcessingInfo {
+    /** Range for which the processing info was reported. */
+    range: Range;
+    /** Kind of progress that was reported. */
+    kind?: CoqFileProgressKind;
+}
+
+interface CoqFileProgressParams {
+    /** 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: CoqFileProgressProcessingInfo[];
+}
+```
+
+#### Changelog
+
+- v1: exact copy from Lean protocol (spec under Apache License)
diff --git a/examples/Pff.v b/examples/Pff.v
@@ -13952,8 +13952,6 @@ apply Rplus_lt_reg_l with (powerRZ radix (t - 1)).
 apply Rle_lt_trans with (2:=W); right;ring.
 Qed.
 
-
-
 Lemma Veltkamp_aux:
    (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\
    (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx')

diff --git a/examples/Rtrigo1.v b/examples/Rtrigo1.v
@@ -1687,4 +1687,4 @@ Proof.
  intros Lo Hi [ -> | -> ].
  - now rewrite cos_PI2.
  - now rewrite cos_3PI2.
-Qed.
+Qed.
diff --git a/examples/ex0.v b/examples/ex0.v
@@ -99,6 +99,4 @@ Proof. by elim: m n p => //= m IHn n p; rewrite IHn. Qed.
 Lemma foobar (n : nat) : n = n.
 Proof. by []. Qed.
 
-Definition muu := 3.
-
-(* End Foo. *)
+Definition muu := 3.
diff --git a/fleche/debug.ml b/fleche/debug.ml
@@ -16,3 +16,6 @@ let parsing = false || all
 
 (* Backtraces *)
 let backtraces = false || all
+
+(* Sched wakeup *)
+let sched_wakeup = true