debug settings

<!-- ps-id: c6aaf75b-0994-4ab7-a173-e9f77c462266 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -12,6 +12,8 @@
    removed, beware of your setup in the extension settings
    (@ejgallego, #208)
  - Settings for the VSCode extension are now categorized (@Alizter, #212)
+ - Debug flags are now configurable in the VSCode extension
+   (@Alizter, #217)
 
 # coq-lsp 0.1.3: Event
 ----------------------

controller/coq_lsp.ml

@@ -86,6 +86,10 @@ end
 
 (* Request Handling: The client expects a reply *)
 module CoqLspOption = struct
+  module Debug = struct
+    type t = [%import: Fleche.Config.Debug.t] [@@deriving yojson]
+  end
+
   type t = [%import: Fleche.Config.t] [@@deriving yojson]
 end
 
@@ -94,7 +98,7 @@ let do_client_options coq_lsp_options : unit =
   LIO.trace_object "init" (`Assoc coq_lsp_options);
   match CoqLspOption.of_yojson (`Assoc coq_lsp_options) with
   | Ok v -> Fleche.Config.v := v
-  | Error msg -> LIO.trace "CoqLspOption.of_yojson error: " msg
+  | Error msg -> LIO.trace "CoqLspOption.of_yojson error" msg
 
 let check_client_version client_version : unit =
   LIO.trace "client_version" client_version;
@@ -117,7 +121,7 @@ let do_initialize ~params =
   do_client_options coq_lsp_options;
   check_client_version !Fleche.Config.v.client_version;
   let client_capabilities = odict_field "capabilities" params in
-  if Fleche.Debug.lsp_init then (
+  if !Fleche.Config.v.debug.lsp_init then (
     LIO.trace "init" "client capabilities:";
     LIO.trace_object "init" (`Assoc client_capabilities));
   let capabilities =
@@ -149,12 +153,12 @@ let answer_request ~ofmt ~id result =
 let postpone_request ~ofmt ~id (pr : PendingRequest.t) =
   match pr with
   | DocRequest { uri; _ } ->
-    if Fleche.Debug.request_delay then
+    if !Fleche.Config.v.debug.request_delay then
       LIO.trace "request" ("postponing rq : " ^ string_of_int id);
     Doc_manager.serve_on_completion ~uri ~id;
     Hashtbl.add rtable id pr
   | PosRequest { uri; point; _ } ->
-    if Fleche.Debug.request_delay then
+    if !Fleche.Config.v.debug.request_delay then
       LIO.trace "request" ("postponing rq : " ^ string_of_int id);
     (* This will go away once we have a proper location request queue in
        Doc_manager *)
@@ -285,7 +289,7 @@ let do_trace params =
 (** Misc helpers *)
 let rec read_request ic =
   let com = LIO.read_request ic in
-  if Fleche.Debug.read then LIO.trace_object "read" com;
+  if !Fleche.Config.v.debug.read then LIO.trace_object "read" com;
   match LSP.Message.from_yojson com with
   | Ok msg -> msg
   | Error msg ->
@@ -299,7 +303,7 @@ let do_cancel ~ofmt ~params =
   cancel_rq ~ofmt ~code ~message id
 
 let serve_postponed ~id pr =
-  if Fleche.Debug.request_delay then
+  if !Fleche.Config.v.debug.request_delay then
     LIO.trace "[wake up]"
       (Format.asprintf "rq: %d | %a" id PendingRequest.data pr);
   match pr with
@@ -461,13 +465,13 @@ let dispatch_or_resume_check ~ofmt ~state =
     LIO.trace "print_bt  [OCaml]" bt
 
 let rec process_queue ofmt ~state =
-  if Fleche.Debug.sched_wakeup then
+  if !Fleche.Config.v.debug.sched_wakeup then
     LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
   dispatch_or_resume_check ~ofmt ~state;
   process_queue ofmt ~state
 
 let process_input (com : LSP.Message.t) =
-  if Fleche.Debug.sched_wakeup then
+  if !Fleche.Config.v.debug.sched_wakeup then
     LIO.trace "-> 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 *)
@@ -511,7 +515,7 @@ let mk_fb_handler q Feedback.{ contents; _ } =
 
 let coq_init ~fb_queue ~bt =
   let fb_handler = mk_fb_handler fb_queue in
-  let debug = bt || Fleche.Debug.backtraces in
+  let debug = bt || !Fleche.Config.v.debug.backtraces in
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
   Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })
@@ -528,13 +532,6 @@ let lsp_main bt coqlib vo_load_path ml_include_path =
   (* IMPORTANT: LSP spec forbids any message from server to client before
      initialize is received *)
 
-  (* Core Coq initialization *)
-  let fb_queue = Coq.Protect.fb_queue in
-  let root_state = coq_init ~fb_queue ~bt in
-  let cmdline =
-    { Coq.Workspace.CmdLine.coqlib; vo_load_path; ml_include_path }
-  in
-
   (* Read JSON-RPC messages and push them to the queue *)
   let rec read_loop () =
     let msg = read_request ic in
@@ -544,9 +541,17 @@ let lsp_main bt coqlib vo_load_path ml_include_path =
 
   (* Input/output will happen now *)
   try
+    (* Core Coq initialization *)
+    let cmdline =
+      { Coq.Workspace.CmdLine.coqlib; vo_load_path; ml_include_path }
+    in
+
     (* LSP Server server initialization *)
     let workspace = lsp_init_loop ic oc ~cmdline in
 
+    let fb_queue = Coq.Protect.fb_queue in
+    let root_state = coq_init ~fb_queue ~bt in
+
     (* Core LSP loop context *)
     let state = { State.root_state; workspace } in