[lsp] Support client-side setting of server options.

This is very convenient as for the user to be able to set server
options that currently require a recompile.

README.md

@@ -100,6 +100,8 @@ possible extensions.
 
 In progress, pending on https://github.com/coq/coq/pull/16261
 
+### Server-side Completion Help
+
 ### "Semantic" goal and document printing
 
 ### LaTeX document support

controller/coq_lsp.ml

@@ -16,8 +16,8 @@
 (************************************************************************)
 
 module F = Format
-module J = Yojson.Basic
-module U = Yojson.Basic.Util
+module J = Yojson.Safe
+module U = Yojson.Safe.Util
 
 let int_field name dict = U.to_int List.(assoc name dict)
 let dict_field name dict = U.to_assoc List.(assoc name dict)
@@ -30,7 +30,7 @@ let _option_empty x =
   | None -> true
   | Some _ -> false
 
-let option_cata f x d =
+let option_cata f d x =
   match x with
   | None -> d
   | Some x -> f x
@@ -40,29 +40,74 @@ let option_default x d =
   | None -> d
   | Some x -> x
 
-let oint_field name dict = option_cata U.to_int List.(assoc_opt name dict) 0
+let oint_field name dict = option_cata U.to_int 0 List.(assoc_opt name dict)
+let ostring_field name dict = Option.map U.to_string (List.assoc_opt name dict)
 
 let odict_field name dict =
   option_default
     U.(to_option to_assoc (option_default List.(assoc_opt name dict) `Null))
     []
 
+module TraceValue = struct
+  type t =
+    | Off
+    | Messages
+    | Verbose
+
+  let parse = function
+    | "messages" -> Messages
+    | "verbose" -> Verbose
+    | "off" -> Off
+    | _ -> raise (Invalid_argument "TraceValue.parse")
+
+  let to_string = function
+    | Off -> "off"
+    | Messages -> "messages"
+    | Verbose -> "verbose"
+end
+
 module LIO = Lsp.Io
 module LSP = Lsp.Base
 
 (* Request Handling: The client expects a reply *)
-let do_initialize ofmt ~id _params =
+module CoqLspOption = struct
+  type t = [%import: Fleche.Config.t] [@@deriving yojson]
+end
+
+let do_client_options coq_lsp_options =
+  LIO.log_error "init" "custom client options:";
+  LIO.log_object "init" (`Assoc coq_lsp_options);
+  match CoqLspOption.of_yojson (`Assoc coq_lsp_options) with
+  | Ok v -> Fleche.Config.v := v
+  | Error _msg -> ()
+
+let do_initialize ofmt ~id params =
+  let coq_lsp_options = odict_field "initializationOptions" params in
+  do_client_options coq_lsp_options;
+  let client_capabilities = odict_field "capabilities" params in
+  LIO.log_error "init" "client capabilities:";
+  LIO.log_object "init" (`Assoc client_capabilities);
+  let trace =
+    ostring_field "trace" params |> option_cata TraceValue.parse TraceValue.Off
+  in
+  LIO.log_error "init" ("trace: " ^ TraceValue.to_string trace);
+  let capabilities =
+    [ ("textDocumentSync", `Int 1)
+    ; ("documentSymbolProvider", `Bool true)
+    ; ("hoverProvider", `Bool true)
+    ; ("completionProvider", `Assoc [])
+    ; ("codeActionProvider", `Bool false)
+    ]
+  in
   let msg =
     LSP.mk_reply ~id
       ~result:
         (`Assoc
-          [ ( "capabilities"
+          [ ("capabilities", `Assoc capabilities)
+          ; ( "serverInfo"
             , `Assoc
-                [ ("textDocumentSync", `Int 1)
-                ; ("documentSymbolProvider", `Bool true)
-                ; ("hoverProvider", `Bool true)
-                ; ("completionProvider", `Assoc [])
-                ; ("codeActionProvider", `Bool false)
+                [ ("name", `String "coq-lsp (C) Inria 2022")
+                ; ("version", `String "0.1+alpha")
                 ] )
           ])
   in
@@ -201,12 +246,12 @@ let do_completion ofmt ~id params =
 (* LIO.log_error "do_completion" (string_of_int line ^"-"^ string_of_int pos) *)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Basic.t =
+let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t =
   let names = List.map (fun id -> `String (Names.Id.to_string id)) names in
   let ty = Pp.string_of_ppcmds ty in
   `Assoc [ ("names", `List names); ("ty", `String ty) ]
 
-let mk_goal { Coq.Goals.info = _; ty; hyps } : Yojson.Basic.t =
+let mk_goal { Coq.Goals.info = _; ty; hyps } : Yojson.Safe.t =
   let ty = Pp.string_of_ppcmds ty in
   `Assoc [ ("ty", `String ty); ("hyps", `List (List.map mk_hyp hyps)) ]
 

controller/dune

@@ -2,5 +2,7 @@
  (name coq_lsp)
  (modules coq_lsp)
  (public_name coq-lsp)
+ (preprocess
+  (staged_pps ppx_import ppx_deriving_yojson))
  (link_flags -linkall)
  (libraries threads coq fleche lsp cmdliner))

editor/code/package.json

@@ -98,6 +98,16 @@
             "items": { "type": "string" },
             "default": [ "--std" ],
             "description": "Arguments to the coq-lsp server"
+          },
+          "coq-lsp.eager_diagnostics": {
+            "type": "boolean",
+            "default": true,
+            "description": "Send diagnostics as document is processed; if false, diagnostics are only sent when Coq finishes processing the file"
+          },
+          "coq-lsp.ok_diagnostics": {
+            "type": "boolean",
+            "default": false,
+            "description": "Send a diagnostic for sentences that are Ok; this can choke vsCode easily due to too many diagnostics"
           }
         }
       }

editor/code/src/client.ts

@@ -8,11 +8,6 @@ let goalPanel : GoalPanel;
 export function activate (context : ExtensionContext) : void {
     window.showInformationMessage('Going to activate!');
 
-    const clientOptions = {
-        documentSelector: [
-            {scheme: 'file', language: 'coq'}
-        ]
-    };
     function coqCommand(command : string, fn : () => void) {
         let disposable = commands.registerCommand('coq-lsp.'+command, fn);
         context.subscriptions.push(disposable);
@@ -25,6 +20,17 @@ export function activate (context : ExtensionContext) : void {
         window.showInformationMessage('Going to start!');
 
         const config = workspace.getConfiguration('coq-lsp');
+        const initializationOptions = {
+            eager_diagnostics: config.eager_diagnostics,
+            ok_diagnostics: config.ok_diagnostics
+        };
+
+        const clientOptions = {
+            documentSelector: [
+                {scheme: 'file', language: 'coq'}
+            ],
+            initializationOptions
+        };
         const serverOptions = { command: config.path, args: config.args };
 
         client = new LanguageClient(

fleche/config.ml

@@ -1,12 +1,20 @@
-(** [mem_stats] Call [Obj.reachable_words] for every sentence. This is very slow
-    and not very useful, so disabled by default *)
-let mem_stats = false
+type t =
+  { mem_stats : bool [@default false]
+        (** [mem_stats] Call [Obj.reachable_words] for every sentence. This is
+            very slow and not very useful, so disabled by default *)
+  ; gc_quick_stats : bool [@default true]
+        (** [gc_quick_stats] Show the diff of [Gc.quick_stats] data for each
+            sentence *)
+  ; eager_diagnostics : bool [@default true]
+        (** [eager_diagnostics] Send (full) diagnostics after processing each *)
+  ; ok_diagnostics : bool [@default false]  (** Show diagnostic for OK lines *)
+  }
 
-(** [gc_quick_stats] Show the diff of [Gc.quick_stats] data for each sentence *)
-let gc_quick_stats = true
+let default =
+  { mem_stats = false
+  ; gc_quick_stats = true
+  ; eager_diagnostics = true
+  ; ok_diagnostics = false
+  }
 
-(** [eager_diagnostics] Send (full) diagnostics after processing each *)
-let eager_diagnostics = true
-
-(** Show diagnostic for OK lines *)
-let ok_diag = false
+let v = ref default

fleche/doc.ml

@@ -182,7 +182,7 @@ let process_and_parse ~uri ~version ~fb_queue doc =
     | Process ast -> (
       let loc = Coq.Ast.loc ast |> Option.get in
       (* XXX Eager update! *)
-      (if Config.eager_diagnostics then
+      (if !Config.v.eager_diagnostics then
        let proc_diag = mk_diag loc 3 (Pp.str "Processing") in
        Io.Report.diagnostics ~uri ~version (proc_diag :: diags));
       (if Debug.parsing then
@@ -201,7 +201,9 @@ let process_and_parse ~uri ~version ~fb_queue doc =
         | Ok { res = state; feedback } ->
           (* let goals = Coq.State.goals *)
           let ok_diag = mk_diag loc 3 (Pp.str "OK") in
-          let diags = if Config.ok_diag then ok_diag :: diags else diags in
+          let diags =
+            if !Config.v.ok_diagnostics then ok_diag :: diags else diags
+          in
           let fb_diags = process_feedback ~loc feedback in
           let diags = fb_diags @ diags in
           let node = { ast; state; memo_info } in
@@ -223,7 +225,7 @@ let process_and_parse ~uri ~version ~fb_queue doc =
   stm doc doc.root []
 
 let print_stats () =
-  (if Config.mem_stats then
+  (if !Config.v.mem_stats then
    let size = Memo.mem_stats () in
    Io.Log.error "stats" (string_of_int size));
 

lsp/base.ml

@@ -22,7 +22,7 @@
 (* Whether to send extended lsp messages *)
 let std_protocol = ref true
 
-module J = Yojson.Basic
+module J = Yojson.Safe
 
 let _mk_extra l = if !std_protocol then [] else l
 

lsp/base.mli

@@ -15,14 +15,14 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-val mk_range : Fleche.Types.Range.t -> Yojson.Basic.t
-val mk_reply : id:int -> result:Yojson.Basic.t -> Yojson.Basic.t
+val mk_range : Fleche.Types.Range.t -> Yojson.Safe.t
+val mk_reply : id:int -> result:Yojson.Safe.t -> Yojson.Safe.t
 
 (* val mk_diagnostic : Range.t * int * string * unit option -> Yojson.Basic.t *)
 val mk_diagnostics :
      uri:string
   -> version:int
   -> (Fleche.Types.Range.t * int * string * unit option) list
-  -> Yojson.Basic.t
+  -> Yojson.Safe.t
 
 val std_protocol : bool ref

lsp/io.ml

@@ -17,7 +17,7 @@
 (************************************************************************)
 
 module F = Format
-module J = Yojson.Basic
+module J = Yojson.Safe
 
 let mut = Mutex.create ()
 let debug_fmt = ref F.err_formatter