[check] Implement fileProgress notification for document progress

CHANGES.md

@@ -13,6 +13,9 @@
  - Don't convert Coq "Info" messages such as "Foo is defined" to
    feedback by default; users willing to see them can set the
    corresponding option (@ejgallego, #113)
+ - 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
 -----------------------

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:

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
+
 let asts_of_doc doc =
   List.filter_map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes
 
@@ -158,7 +173,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
@@ -186,7 +203,6 @@ 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);
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
   | [] -> ()
@@ -195,12 +211,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
@@ -352,6 +374,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;
@@ -402,6 +426,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
@@ -429,6 +455,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) =

editor/code/package.json

@@ -9,7 +9,6 @@
     "Shachar Itzhaky <shachari@cs.technion.ac.il>",
     "Ramkumar Ramachandra <r@artagnon.com>"
   ],
-
   "publisher": "ejgallego",
   "engines": {
     "vscode": "^1.73.0"
@@ -131,11 +130,13 @@
   },
   "devDependencies": {
     "@types/node": "^10.14.15",
+    "@types/throttle-debounce": "^5.0.0",
     "@types/vscode": "^1.73.0",
     "esbuild": "^0.15.14",
     "typescript": "^4.8.4"
   },
   "dependencies": {
+    "throttle-debounce": "^5.0.0",
     "vscode-languageclient": "^8.0.2"
   },
   "main": "./out/src/client.js",

editor/code/src/client.ts

@@ -1,3 +1,4 @@
+import { throttle } from "throttle-debounce";
 import {
     window,
     commands,
@@ -6,13 +7,17 @@ import {
     ViewColumn,
     Uri,
     TextEditor,
+    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;
@@ -45,7 +50,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 = {
@@ -69,16 +74,37 @@ 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);
+            updateDecos(params.textDocument.uri, 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 updateDecos = throttle(200,
+        function(uri : string, ranges : vscode.Range[]) {
+            for (const editor of window.visibleTextEditors) {
+                if (editor.document.uri.toString() == uri) {
+                    editor.setDecorations(progressDecoration, ranges);
+                }
+            }
+        });
+
+    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);
         }
     };
-    
+
     const goals = (editor : TextEditor) => {
         checkPanelAlive();
         let uri = editor.document.uri;

editor/code/src/goals.ts

@@ -10,6 +10,7 @@ interface Goal {
     ty: string;
     hyps: Hyp[];
 }
+
 interface GoalRequest {}
 
 // returns the HTML code of goals environment

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');