Merge branch 'main' into v8.18

CHANGES.md

@@ -38,6 +38,12 @@
    (@ejgallego, #616)
  - completion: correctly understand UTF-16 code points on completion
    request (Léo Stefanesco, #613, fixes #531)
+ - 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
 -------------------------------

README.md

@@ -424,7 +424,11 @@ The license for this project is LGPL 2.1 (or GPL 3+ as stated in the LGPL 2.1).
 Work on this server has been made possible thanks to many discussions,
 inspirations, and sharing of ideas from colleagues. In particular, we'd like to
 thank Rudi Grinberg, Andrey Mokhov, Clément Pit-Claudel, and Makarius Wenzel for
-their help and advice.
+their help and advice. Gaëtan Gilbert contributed many key and challenging Coq
+patches essential to `coq-lsp`; we also thank Guillaume Munch-Maccagnoni for his
+[memprof-limits](https://guillaume.munch.name/software/ocaml/memprof-limits/index.html)
+library, which is essential to make `coq-lsp` on the real world, as well for
+many advice w.r.t. OCaml.
 
 As noted above, the original implementation was based on the Lambdapi LSP
 server, thanks to all the collaborators in that project!

controller/lsp_core.ml

@@ -361,14 +361,19 @@ let do_completion =
   do_position_request ~postpone:true ~handler:Rq_completion.completion
 
 (* Requires the full document to be processed *)
-let do_document_request ~params ~handler =
+let do_document_request ~postpone ~params ~handler =
   let uri = Helpers.get_uri params in
-  Rq.Action.Data (Request.Data.DocRequest { uri; handler })
+  Rq.Action.Data (Request.Data.DocRequest { uri; postpone; handler })
 
-let do_symbols = do_document_request ~handler:Rq_symbols.symbols
-let do_document = do_document_request ~handler:Rq_document.request
-let do_save_vo = do_document_request ~handler:Rq_save.request
-let do_lens = do_document_request ~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

controller/request.ml

@@ -48,6 +48,7 @@ module Data = struct
   type t =
     | DocRequest of
         { uri : Lang.LUri.File.t
+        ; postpone : bool
         ; handler : document
         }
     | PosRequest of
@@ -60,7 +61,8 @@ module Data = struct
 
   (* Debug printing *)
   let data fmt = function
-    | DocRequest { uri = _; handler = _ } -> Format.fprintf fmt "{k:doc}"
+    | DocRequest { uri = _; postpone; handler = _ } ->
+      Format.fprintf fmt "{k:doc | p: %B}" postpone
     | PosRequest { uri = _; point; version; postpone; handler = _ } ->
       Format.fprintf fmt "{k:pos | l: %d, c: %d v: %a p: %B}" (fst point)
         (snd point)
@@ -69,13 +71,14 @@ module Data = struct
 
   let dm_request pr =
     match pr with
-    | DocRequest { uri; handler = _ } -> Fleche.Theory.Request.(FullDoc { uri })
+    | DocRequest { uri; postpone; handler = _ } ->
+      Fleche.Theory.Request.(FullDoc { uri; postpone })
     | PosRequest { uri; point; version; postpone; handler = _ } ->
       Fleche.Theory.Request.(PosInDoc { uri; point; version; postpone })
 
   let serve ~doc pr =
     match pr with
-    | DocRequest { uri = _; handler } -> handler ~doc
+    | DocRequest { uri = _; postpone = _; handler } -> handler ~doc
     | PosRequest { uri = _; point; version = _; postpone = _; handler } ->
       handler ~point ~doc
 end

controller/request.mli

@@ -33,6 +33,7 @@ module Data : sig
   type t =
     | DocRequest of
         { uri : Lang.LUri.File.t
+        ; postpone : bool
         ; handler : document
         }
     | PosRequest of

coq-lsp.opam

@@ -30,8 +30,8 @@ depends: [
   # waterproof parser
   "menhir"       { >= "20220210" }
 
-  # for unit testing
-  "alcotest"     { >= "1.6.0" & with-test }
+  # unit testing
+  "ppx_inline_test"     { >= "0.14.1" }
 
   # Uncomment this for releases
   "coq"          { >= "8.18" < "8.19"  }

coq/dune

@@ -3,4 +3,7 @@
  (public_name coq-lsp.coq)
  ; Unfortunate we have to link the STM due to the LTAC plugin
  ; depending on it, we should fix this upstream
+ (inline_tests)
+ (preprocess
+  (pps ppx_inline_test))
  (libraries lang coq-core.vernac coq-serapi.serlib))

coq/protect.mli

@@ -11,6 +11,9 @@ module Error : sig
     | Anomaly of 'l payload
 end
 
+(** This "monad" could be related to "Runners in action" (Ahman,
+    Bauer), thanks to Guillaume Munch-Maccagnoni for the reference and
+    for many useful tips! *)
 module R : sig
   type ('a, 'l) t = private
     | Completed of ('a, 'l Error.t) result

coq/utf8.ml

@@ -189,3 +189,31 @@ let get_byte_offset_from_utf16_pos line (char : int) =
     ()
   done;
   if !byte_idx < String.length line then Some !byte_idx else None
+
+let%test_unit "utf16 offsets" =
+  let testcases_x =
+    [ ("aax", 2, true)
+    ; ("  xoo", 2, true)
+    ; ("0123", 4, false)
+    ; ("  𝒞x", 4, true)
+    ; ("  𝒞x𝒞", 4, true)
+    ; ("  𝒞∫x", 5, true)
+    ; ("  𝒞", 4, false)
+    ; ("∫x.dy", 1, true)
+    ]
+  in
+  List.iter
+    (fun (s, i, b) ->
+      let res = get_byte_offset_from_utf16_pos s i in
+      if b then
+        let res = Option.map (fun i -> s.[i]) res in
+        match res with
+        | Some x when x = 'x' -> ()
+        | Some x ->
+          failwith
+            (Printf.sprintf "Didn't find x in test %s : %d, instead: %c" s i x)
+        | None ->
+          failwith (Printf.sprintf "Didn't not find x in test %s : %d" s i)
+      else if res != None then
+        failwith (Printf.sprintf "Shouldn't find x in test %s : %d" s i))
+    testcases_x

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/client.ts

@@ -12,6 +12,8 @@ import {
   ThemeColor,
   WorkspaceConfiguration,
   Disposable,
+  DocumentSelector,
+  languages,
 } from "vscode";
 
 import {
@@ -29,7 +31,11 @@ import {
   GoalAnswer,
   PpString,
 } from "../lib/types";
-import { CoqLspClientConfig, CoqLspServerConfig } from "./config";
+import {
+  CoqLspClientConfig,
+  CoqLspServerConfig,
+  coqLSPDocumentSelector,
+} from "./config";
 import { InfoPanel, goalReq } from "./goals";
 import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
@@ -208,10 +214,8 @@ export function activateCoqLSP(
     textEditor: TextEditor,
     callKind: TextEditorSelectionChangeKind | undefined
   ) => {
-    if (
-      textEditor.document.languageId != "coq" &&
-      textEditor.document.languageId != "markdown"
-    )
+    // Don't trigger the goals if the buffer is not owned by us
+    if (languages.match(coqLSPDocumentSelector, textEditor.document) < 1)
       return;
 
     const kind =

editor/code/src/config.ts

@@ -1,4 +1,4 @@
-import { ExtensionContext, workspace } from "vscode";
+import { DocumentSelector, ExtensionContext, workspace } from "vscode";
 
 export interface CoqLspServerConfig {
   client_version: string;
@@ -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,
     };
   }
 }
@@ -54,3 +56,7 @@ export namespace CoqLspClientConfig {
     return obj;
   }
 }
+export const coqLSPDocumentSelector: DocumentSelector = [
+  { language: "coq" },
+  { language: "markdown", pattern: "**/*.mv" },
+];

editor/code/src/progress.ts

@@ -1,10 +1,17 @@
 import { throttle } from "throttle-debounce";
-import { Disposable, Range, window, OverviewRulerLane } from "vscode";
+import {
+  Disposable,
+  Range,
+  window,
+  OverviewRulerLane,
+  languages,
+} from "vscode";
 import {
   NotificationType,
   VersionedTextDocumentIdentifier,
 } from "vscode-languageclient";
 import { BaseLanguageClient } from "vscode-languageclient";
+import { coqLSPDocumentSelector } from "./config";
 
 enum CoqFileProgressKind {
   Processing = 1,
@@ -64,10 +71,7 @@ export class FileProgressManager {
   });
   private cleanDecos() {
     for (const editor of window.visibleTextEditors) {
-      if (
-        editor.document.languageId === "coq" ||
-        editor.document.languageId === "markdown"
-      ) {
+      if (languages.match(coqLSPDocumentSelector, editor.document) > 0) {
         editor.setDecorations(progressDecoration, []);
       }
     }