[fleche] Auto-check documents on scroll when in lazy mode.

CHANGES.md

@@ -111,6 +111,7 @@
    (@ejgallego, @Alizter, #689, #693)
  - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
  - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
+ - New cleint option to enable / disable `coq/perfData` (@ejgallego, #717)
  - The `coq-lsp.document` VSCode command will now display the returned
    JSON data in a new editor (@ejgallego, #701)
  - New server option to enable / disable `coq/perfData` (@ejgallego,
@@ -130,6 +131,10 @@
    changes in some part of the document (@ejgallego, #709)
  - JSON-RPC library now supports all kind of incoming messages
    (@ejgallego, #713)
+ - New `coq/viewRange` notification, from client to server, than hints
+   the scheduler for the visible area of the document; combined with
+   the new lazy checking mode, this provides checking on scroll, a
+   feature inspired from Isabelle IDE (@ejgallego, #717)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

controller/lsp_core.ml

@@ -411,6 +411,17 @@ let do_cancel ~ofn ~params =
 
 let do_cache_trim () = Nt_cache_trim.notification ()
 
+let do_viewRange params =
+  match List.assoc "range" params |> Lsp.JLang.Diagnostic.Range.of_yojson with
+  | Ok range ->
+    let { Lsp.JLang.Diagnostic.Range.end_ = { line; character }; _ } = range in
+    let message = Format.asprintf "l: %d c:%d" line character in
+    LIO.trace "viewRange" message;
+    let uri = Helpers.get_uri params in
+    Fleche.Theory.Check.set_scheduler_hint ~uri ~point:(line, character);
+    ()
+  | Error err -> LIO.trace "viewRange" ("error in parsing notification: " ^ err)
+
 let do_changeConfiguration params =
   let message = "didChangeReceived" in
   let () = LIO.(logMessage ~lvl:Lvl.Info ~message) in
@@ -496,6 +507,7 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
   | "textDocument/didClose" -> do_close ~ofn params
   | "textDocument/didSave" -> Cache.save_to_disk ()
   (* Specific to coq-lsp *)
+  | "coq/viewRange" -> do_viewRange params
   | "coq/trimCaches" -> do_cache_trim ()
   (* Cancel Request *)
   | "$/cancelRequest" -> do_cancel ~ofn ~params

editor/code/lib/types.ts

@@ -179,3 +179,8 @@ export type PerfMessagePayload = PerfUpdate | PerfReset;
 export interface PerfMessageEvent extends MessageEvent {
   data: PerfMessagePayload;
 }
+
+export interface ViewRangeParams {
+  textDocument: VersionedTextDocumentIdentifier;
+  range: Range;
+}

editor/code/package.json

@@ -283,7 +283,12 @@
           "coq-lsp.check_only_on_request": {
             "type": "boolean",
             "default": false,
-            "description": "Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded. Note that this option is experimental and not recommended for use yet; we expose it only for testing and further development."
+            "description": "Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded. Note that this feature is experimental."
+          },
+          "coq-lsp.check_on_scroll": {
+            "type": "boolean",
+            "default": false,
+            "description": "When in lazy mode, check files on scroll. Note that this feature is experimental."
           }
         }
       },

editor/code/src/client.ts

@@ -14,6 +14,7 @@ import {
   Disposable,
   languages,
   Uri,
+  TextEditorVisibleRangesChangeEvent,
 } from "vscode";
 
 import * as vscode from "vscode";
@@ -37,6 +38,7 @@ import {
   GoalAnswer,
   PpString,
   DocumentPerfParams,
+  ViewRangeParams,
 } from "../lib/types";
 
 import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config";
@@ -45,6 +47,7 @@ import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
 import { sentenceNext, sentenceBack } from "./edit";
 import { HeatMap, HeatMapConfig } from "./heatmap";
+import { debounce, throttle } from "throttle-debounce";
 
 // Convert perf data to VSCode format
 function toVsCodePerf(
@@ -314,6 +317,29 @@ export function activateCoqLSP(
 
   context.subscriptions.push(goalsHook);
 
+  const viewRangeNotification = new NotificationType<ViewRangeParams>(
+    "coq/viewRange"
+  );
+
+  let viewRangeHook = window.onDidChangeTextEditorVisibleRanges(
+    throttle(400, (evt: TextEditorVisibleRangesChangeEvent) => {
+      if (
+        config.check_on_scroll &&
+        languages.match(CoqSelector.local, evt.textEditor.document) > 0 &&
+        evt.visibleRanges[0]
+      ) {
+        let uri = evt.textEditor.document.uri.toString();
+        let version = evt.textEditor.document.version;
+        let textDocument = { uri, version };
+        let range = client.code2ProtocolConverter.asRange(evt.visibleRanges[0]);
+        let params: ViewRangeParams = { textDocument, range };
+        client.sendNotification(viewRangeNotification, params);
+      }
+    })
+  );
+
+  context.subscriptions.push(viewRangeHook);
+
   // Heatmap setup
   heatMap = new HeatMap(
     workspace.getConfiguration("coq-lsp").get("heatmap") as HeatMapConfig

editor/code/src/config.ts

@@ -14,6 +14,7 @@ export interface CoqLspServerConfig {
   show_stats_on_hover: boolean;
   show_loc_info_on_hover: boolean;
   check_only_on_request: boolean;
+  send_perf_data: boolean;
 }
 
 export namespace CoqLspServerConfig {
@@ -35,6 +36,7 @@ export namespace CoqLspServerConfig {
       show_stats_on_hover: wsConfig.show_stats_on_hover,
       show_loc_info_on_hover: wsConfig.show_loc_info_on_hover,
       check_only_on_request: wsConfig.check_only_on_request,
+      send_perf_data: wsConfig.send_perf_data,
     };
   }
 }
@@ -49,6 +51,7 @@ export enum ShowGoalsOnCursorChange {
 export interface CoqLspClientConfig {
   show_goals_on: ShowGoalsOnCursorChange;
   pp_format: "Pp" | "Str";
+  check_on_scroll: boolean;
 }
 
 function pp_type_to_pp_format(pp_type: 0 | 1 | 2): "Pp" | "Str" {
@@ -67,6 +70,7 @@ export namespace CoqLspClientConfig {
     let obj: CoqLspClientConfig = {
       show_goals_on: wsConfig.show_goals_on,
       pp_format: pp_type_to_pp_format(wsConfig.pp_type),
+      check_on_scroll: wsConfig.check_on_scroll,
     };
     return obj;
   }

etc/doc/PROTOCOL.md

@@ -354,6 +354,18 @@ const coqPerfData : NotificationType<DocumentPerfParams<Range>>
 The `coq/trimCaches` notification from client to server tells the
 server to free memory. It has no parameters.
 
+### Viewport notification
+
+The `coq/viewRange` notification from client to server tells the
+server the visible range of the user.
+
+```typescript
+interface ViewRangeParams {
+  textDocument: VersionedTextDocumentIdentifier;
+  range: Range;
+}
+```
+
 ### Did Change Configuration and Server Configuration parameters
 
 The server will listen to the `workspace/didChangeConfiguration`

etc/doc/USER_MANUAL.md

@@ -24,25 +24,56 @@ facilities. In VSCode, these settings can be usually displayed in the
 
 ## Key features:
 
+### Continuous vs on-demand mode
+
+`coq-lsp` offers two checking modes:
+
+- continuous checking [default]: `coq-lsp` will check all your open
+  documents eagerly. This is best when working with powerful machines
+  to minimize latency. When using OCaml 4.x, `coq-lsp` uses the
+  `memprof-limits` library to interrupt Coq and stay responsive.
+
+- on-demand checking [set the `check_only_on_request` option]: In this
+  mode, `coq-lsp` will stay idle and only compute information that is
+  demanded, for example, when the user asks for goals. This mode
+  disables some useful features such as `documentSymbol` as they can
+  only be implemented by checking the full file.
+
+  This mode provides the `check_on_scroll` option, which improves
+  latency by telling `coq-lsp` to check eagerly what is on view on
+  user's screen.
+
+### Goal display
+
+By default, `coq-lsp` will follow cursor and show goals at cursor
+position. This can be tweaked in options. There are commands to move
+one Coq sentence forward / backwards.
+
 ### Incremental proof edition
 
-`coq-lsp` will recognize blocks of the form:
+Once you have setup your basic proof style, you may want to work with
+`coq-lsp` in a way that is friendly to incremental checking.
+
+For example, `coq-lsp` will recognize blocks of the form:
 ```coq
 Lemma foo : T.
 Proof.
  ...
 Qed.
 ```
 
-and will allow you to edit inside the `Proof.` `Qed.` block without rechecing what is outside.
+and will allow you to edit inside the `Proof.` `Qed.` block without
+re-checking what is outside.
 
 ### Error recovery
 
 `coq-lsp` can recover many errors automatically and allow you to
 continue document edition later on.
 
 For example, it is not necessary to put `Admitted` in proofs that are
-not fully completed.
+not fully completed. Also, you can work with bullets and `coq-lsp`
+will automatically admit unfinished ones, so you can follow the
+natural proof structure.
 
 ## Settings
 

fleche/theory.ml

@@ -194,6 +194,8 @@ module Check : sig
 
   val maybe_check :
     io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+
+  val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit
 end = struct
   let pending = ref []
 
@@ -214,9 +216,18 @@ end = struct
       | None -> pend_try f tt
       | Some r -> Some r)
 
+  let hint : (int * int) option ref = ref None
+
   let get_check_target pt_requests =
     let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
-    Option.map target_of_pt_handle (List.nth_opt pt_requests 0)
+    match Option.map target_of_pt_handle (List.nth_opt pt_requests 0) with
+    | None ->
+      Option.map
+        (fun (l, c) ->
+          hint := None;
+          Doc.Target.Position (l, c))
+        !hint
+    | Some t -> Some t
 
   (* Notification handling; reply is optional / asynchronous *)
   let check ~io ~token ~uri =
@@ -255,6 +266,12 @@ end = struct
 
   let deschedule ~uri =
     pending := CList.remove Lang.LUri.File.equal uri !pending
+
+  let set_scheduler_hint ~uri ~point =
+    if CList.is_empty !pending then
+      let () = hint := Some point in
+      schedule ~uri (* if the hint is set we wanna override it *)
+    else if not (Option.is_empty !hint) then hint := Some point
 end
 
 let create ~io ~token ~env ~uri ~raw ~version =

fleche/theory.mli

@@ -21,6 +21,8 @@ module Check : sig
       progress and diagnostics notifications using output function [ofn]. *)
   val maybe_check :
     io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+
+  val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit
 end
 
 (** Create a document inside a theory *)

lsp/jLang.mli

@@ -21,6 +21,22 @@ end
 
 module Diagnostic : sig
   type t = Lang.Diagnostic.t [@@deriving to_yojson]
+
+  module Point : sig
+    type t =
+      { line : int
+      ; character : int
+      }
+    [@@deriving yojson]
+  end
+
+  module Range : sig
+    type t =
+      { start : Point.t
+      ; end_ : Point.t [@key "end"]
+      }
+    [@@deriving yojson]
+  end
 end
 
 val mk_diagnostics :