[fleche] Experimental option for "lazy" document checking.

CHANGES.md

@@ -41,6 +41,9 @@
  - don't trigger the goals window in general markdown buffer
    (@ejgallego, #625, reported by Théo Zimmerman)
  - allow not to postpone full document requests (#626, @ejgallego)
+ - new configuration value `check_only_on_request` which will delay
+   checking the document until a request has been made (#629, cc: #24,
+   @ejgallego)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------

controller/lsp_core.ml

@@ -365,13 +365,15 @@ let do_document_request ~postpone ~params ~handler =
   let uri = Helpers.get_uri params in
   Rq.Action.Data (Request.Data.DocRequest { uri; postpone; handler })
 
-let do_symbols = do_document_request ~postpone:true ~handler:Rq_symbols.symbols
-
-let do_document =
-  do_document_request ~postpone:true ~handler:Rq_document.request
-
-let do_save_vo = do_document_request ~postpone:true ~handler:Rq_save.request
-let do_lens = do_document_request ~postpone:true ~handler:Rq_lens.request
+(* Don't postpone when in lazy mode *)
+let do_document_request_maybe ~params ~handler =
+  let postpone = not !Fleche.Config.v.check_only_on_request in
+  do_document_request ~postpone ~params ~handler
+
+let do_symbols = do_document_request_maybe ~handler:Rq_symbols.symbols
+let do_document = do_document_request_maybe ~handler:Rq_document.request
+let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
+let do_lens = do_document_request_maybe ~handler:Rq_lens.request
 
 let do_cancel ~ofn ~params =
   let id = int_field "id" params in

editor/code/package.json

@@ -259,6 +259,13 @@
             "default": true,
             "description": "If a `Qed.` command fails, admit the proof automatically."
           }
+        },
+        "properties": {
+          "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."
+          }
         }
       },
       {

editor/code/src/config.ts

@@ -13,6 +13,7 @@ export interface CoqLspServerConfig {
   pp_type: 0 | 1 | 2;
   show_stats_on_hover: boolean;
   show_loc_info_on_hover: boolean;
+  check_only_on_request: boolean;
 }
 
 export namespace CoqLspServerConfig {
@@ -33,6 +34,7 @@ export namespace CoqLspServerConfig {
       pp_type: wsConfig.pp_type,
       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,
     };
   }
 }

fleche/config.ml

@@ -48,6 +48,7 @@ type t =
   ; verbosity : int [@default 2]
         (** Verbosity, 1 = reduced, 2 = default. As of today reduced will
             disable all logging, and the diagnostics and perf_data notification *)
+  ; check_only_on_request : bool [@default false]
   }
 
 let default =
@@ -69,6 +70,7 @@ let default =
   ; pp_json = false
   ; send_perf_data = true
   ; send_diags = true
+  ; check_only_on_request = false
   }
 
 let v = ref default

fleche/theory.ml

@@ -196,21 +196,31 @@ end = struct
 
   let get_check_target pt_requests =
     let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
-    Option.cata target_of_pt_handle Doc.Target.End (List.nth_opt pt_requests 0)
+    Option.map target_of_pt_handle (List.nth_opt pt_requests 0)
 
   (* Notification handling; reply is optional / asynchronous *)
   let check ~io ~uri =
     Io.Log.trace "process_queue" "resuming document checking";
     match Handle.find_opt ~uri with
-    | Some handle ->
+    | Some handle -> (
       let target = get_check_target handle.pt_requests in
-      let doc = Doc.check ~io ~target ~doc:handle.doc () in
-      let requests = Handle.update_doc_info ~handle ~doc in
-      if Doc.Completion.is_completed doc.completed then Register.fire ~io ~doc;
-      (* Remove from the queu *)
-      if Doc.Completion.is_completed doc.completed then
+      match target with
+      (* If we are in lazy mode and we don't have any full document requests
+         pending, we just deschedule *)
+      | None
+        when !Config.v.check_only_on_request
+             && Int.Set.is_empty handle.cp_requests ->
         pending := pend_pop !pending;
-      Some (requests, doc)
+        None
+      | (None | Some _) as tgt ->
+        let target = Option.default Doc.Target.End tgt in
+        let doc = Doc.check ~io ~target ~doc:handle.doc () in
+        let requests = Handle.update_doc_info ~handle ~doc in
+        if Doc.Completion.is_completed doc.completed then Register.fire ~io ~doc;
+        (* Remove from the queue *)
+        if Doc.Completion.is_completed doc.completed then
+          pending := pend_pop !pending;
+        Some (requests, doc))
     | None ->
       pending := pend_pop !pending;
       Io.Log.trace "Check.check"