debug settings

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

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

CHANGES.md

@@ -17,6 +17,9 @@
    (@ejgallego, #237)
  - In `_CoqProject`, `-impredicative-set` is now parsed correctly
    (@artagnon, #241)
+ - Debug flags are now configurable in the VSCode extension
+   (@Alizter, #217)
+ - The -bt flag has been removed. (Alizter, #217)
 
 # coq-lsp 0.1.3: Event
 ----------------------

controller/coq_lsp.ml

@@ -90,7 +90,7 @@ module Rq = struct
   let _rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673
 
   let postpone ~id (pr : PendingRequest.t) =
-    if Fleche.Debug.request_delay then
+    if !Fleche.Config.v.debug.request_delay then
       LIO.trace "request" ("postponing rq : " ^ string_of_int id);
     PendingRequest.postpone ~id pr;
     Hashtbl.add _rtable id pr
@@ -114,7 +114,7 @@ module Rq = struct
     consume_ ~ofmt ~f id
 
   let debug_wakeup 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)
 
@@ -255,7 +255,7 @@ let do_cancel ~ofmt ~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 ->
@@ -401,13 +401,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 *)
@@ -449,14 +449,13 @@ let mk_fb_handler q Feedback.{ contents; _ } =
   | Message (Debug, _loc, _msg) -> ()
   | _ -> ()
 
-let coq_init ~fb_queue ~bt =
+let coq_init ~fb_queue =
   let fb_handler = mk_fb_handler fb_queue in
-  let debug = bt || Fleche.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 })
+  Coq.Init.(coq_init { fb_handler; load_module; load_plugin })
 
-let lsp_main bt coqlib vo_load_path ml_include_path =
+let lsp_main coqlib vo_load_path ml_include_path =
   (* We output to stdout *)
   let ic = stdin in
   let oc = F.std_formatter in
@@ -470,13 +469,14 @@ let lsp_main bt coqlib vo_load_path ml_include_path =
 
   (* Core Coq initialization *)
   let fb_queue = Coq.Protect.fb_queue in
-  let root_state = coq_init ~fb_queue ~bt in
+  let root_state = coq_init ~fb_queue 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 () =
+    Exninfo.record_backtrace !Fleche.Config.v.debug.backtraces;
     let msg = read_request ic in
     process_input msg;
     read_loop ()
@@ -516,10 +516,6 @@ let lsp_main bt coqlib vo_load_path ml_include_path =
 (* Arguments handling *)
 open Cmdliner
 
-let bt =
-  let doc = "Enable backtraces" in
-  Cmdliner.Arg.(value & flag & info [ "bt" ] ~doc)
-
 let coq_lp_conv ~implicit (unix_path, lp) =
   { Loadpath.coq_path = Libnames.dirpath_of_string lp
   ; unix_path
@@ -580,7 +576,7 @@ let lsp_cmd : unit Cmd.t =
   Cmd.(
     v
       (Cmd.info "coq-lsp" ~version:Version.server ~doc ~man)
-      Term.(const lsp_main $ bt $ coqlib $ vo_load_path $ ml_include_path))
+      Term.(const lsp_main $ coqlib $ vo_load_path $ ml_include_path))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in

controller/rq_init.ml

@@ -21,6 +21,10 @@ let odict_field name dict =
 
 (* 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
 
@@ -52,7 +56,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 =

coq/init.ml

@@ -24,7 +24,6 @@ type coq_opts =
   ; load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
-  ; debug : bool  (** Enable Coq Debug mode *)
   }
 
 let coq_init opts =
@@ -33,8 +32,6 @@ let coq_init opts =
   Global.set_impredicative_set false;
   Global.set_native_compiler false;
 
-  if opts.debug then CDebug.set_flags "backtrace";
-
   (**************************************************************************)
   (* Feedback setup                                                         *)
   (**************************************************************************)

coq/init.mli

@@ -24,7 +24,6 @@ type coq_opts =
   ; load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
-  ; debug : bool  (** Enable Coq Debug mode *)
   }
 
 val coq_init : coq_opts -> State.t

editor/code/src/config.ts

@@ -1,25 +1,44 @@
-import { ExtensionContext, workspace } from "vscode";
+interface CoqLspServerDebugConfig {
+  cache: boolean;
+  send: boolean;
+  read: boolean;
+  lsp_init: boolean;
+  parsing: boolean;
+  scan: boolean;
+  backtraces: boolean;
+  unicode: boolean;
+  sched_wakeup: boolean;
+  request_delay: boolean;
+  mem_stats: boolean;
+  gc_quick_stats: boolean;
+}
 
-export interface CoqLspServerConfig {
+interface CoqLspServerConfig {
   client_version: string;
+  mem_stats: boolean;
+  gc_quick_stats: boolean;
   eager_diagnostics: boolean;
   ok_diagnostics: boolean;
   goal_after_tactic: boolean;
   show_coq_info_messages: boolean;
   show_notices_as_diagnostics: boolean;
   admit_on_bad_qed: boolean;
+  debug: CoqLspServerDebugConfig;
 }
 
 export namespace CoqLspServerConfig {
   export function create(client_version: string, wsConfig: any) {
     return {
       client_version: client_version,
+      mem_stats: wsConfig.mem_stats,
+      gc_quick_stats: wsConfig.gc_quick_stats,
       eager_diagnostics: wsConfig.eager_diagnostics,
       ok_diagnostics: wsConfig.ok_diagnostics,
       goal_after_tactic: wsConfig.goal_after_tactic,
       show_coq_info_messages: wsConfig.show_coq_info_messages,
       show_notices_as_diagnostics: wsConfig.show_notices_as_diagnostics,
       admit_on_bad_qed: wsConfig.admit_on_bad_qed,
+      debug: wsConfig.debug,
     };
   }
 }

fleche/config.ml

@@ -1,38 +1,87 @@
+module Debug = struct
+  type t =
+    { cache : bool
+    ; send : bool
+    ; read : bool
+    ; lsp_init : bool
+    ; parsing : bool
+    ; scan : bool
+    ; backtraces : bool
+    ; unicode : bool
+    ; sched_wakeup : bool
+    ; request_delay : bool
+    ; mem_stats : bool
+    ; gc_quick_stats : bool
+    }
+
+  let all =
+    { cache = true
+    ; send = true
+    ; read = true
+    ; lsp_init = true
+    ; parsing = true
+    ; scan = true
+    ; backtraces = true
+    ; unicode = true
+    ; sched_wakeup = true
+    ; request_delay = true
+    ; mem_stats = true
+    ; gc_quick_stats = true
+    }
+
+  let none =
+    { cache = false
+    ; send = false
+    ; read = false
+    ; lsp_init = false
+    ; parsing = false
+    ; scan = false
+    ; backtraces = false
+    ; unicode = false
+    ; sched_wakeup = false
+    ; request_delay = false
+    ; mem_stats = false
+    ; gc_quick_stats = false
+    }
+
+  let lsp =
+    { cache = false
+    ; send = true
+    ; read = true
+    ; lsp_init = true
+    ; parsing = false
+    ; scan = false
+    ; backtraces = false
+    ; unicode = false
+    ; sched_wakeup = false
+    ; request_delay = false
+    ; mem_stats = false
+    ; gc_quick_stats = true
+    }
+end
+
 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 *)
-  ; client_version : string [@default "any"]
-  ; eager_diagnostics : bool [@default true]
-        (** [eager_diagnostics] Send (full) diagnostics after processing each *)
-  ; ok_diagnostics : bool [@default false]  (** Show diagnostic for OK lines *)
-  ; goal_after_tactic : bool [@default false]
-        (** When showing goals and the cursor is in a tactic, if false, show
-            goals before executing the tactic, if true, show goals after *)
-  ; show_coq_info_messages : bool [@default false]
-        (** Show `msg_info` messages in diagnostics *)
-  ; show_notices_as_diagnostics : bool [@default false]
-        (** Show `msg_notice` messages in diagnostics *)
-  ; admit_on_bad_qed : bool [@default true]
-        (** [admit_on_bad_qed] There are two possible error recovery strategies
-            when a [Qed] fails: one is not to add the constant to the state, the
-            other one is admit it. We find the second behavior more useful, but
-            YMMV. *)
+  { client_version : string
+  ; eager_diagnostics : bool
+  ; ok_diagnostics : bool
+  ; goal_after_tactic : bool
+  ; show_coq_info_messages : bool
+  ; show_notices_as_diagnostics : bool
+  ; admit_on_bad_qed : bool
+  ; debug : Debug.t
   }
 
 let default =
-  { mem_stats = false
-  ; gc_quick_stats = true
-  ; client_version = "any"
+  { client_version = "any"
   ; eager_diagnostics = true
   ; ok_diagnostics = false
   ; goal_after_tactic = false
   ; show_coq_info_messages = false
   ; show_notices_as_diagnostics = false
   ; admit_on_bad_qed = true
+  ; debug = Debug.none
   }
 
 let v = ref default
+let debug_all () = v := { !v with debug = Debug.all }
+let debug_lsp () = v := { !v with debug = Debug.lsp }

fleche/config.mli

@@ -0,0 +1,67 @@
+module Debug : sig
+  (** Debug configuration *)
+
+  type t =
+    { cache : bool [@default false]  (** Debug info about caching. *)
+    ; send : bool [@default false]  (** LSP messages: Send and receive *)
+    ; read : bool [@default false]
+    ; lsp_init : bool [@default false]
+          (** Parsing (this is a bit expensive as it will call the printer *)
+    ; parsing : bool [@default false]  (** scanning of prefix-incrementality *)
+    ; scan : bool [@default false]  (** Backtraces *)
+    ; backtraces : bool [@default false]  (** Unicode conversion *)
+    ; unicode : bool [@default false]  (** Sched wakeup *)
+    ; sched_wakeup : bool [@default false]  (** Request event queue *)
+    ; request_delay : bool [@default true]
+    ; mem_stats : bool [@default false] (* TODO: unused? *)
+          (** [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 *)
+    }
+end
+
+type t =
+  { client_version : string [@default "any"]
+  ; eager_diagnostics : bool [@default true]
+        (** [eager_diagnostics] Send (full) diagnostics after processing each *)
+  ; ok_diagnostics : bool [@default false]  (** Show diagnostic for OK lines *)
+  ; goal_after_tactic : bool [@default false]
+        (** When showing goals and the cursor is in a tactic, if false, show
+            goals before executing the tactic, if true, show goals after *)
+  ; show_coq_info_messages : bool [@default false]
+        (** Show `msg_info` messages in diagnostics *)
+  ; show_notices_as_diagnostics : bool [@default false]
+        (** Show `msg_notice` messages in diagnostics *)
+  ; admit_on_bad_qed : bool [@default true]
+        (** [admit_on_bad_qed] There are two possible error recovery strategies
+            when a [Qed] fails: one is not to add the constant to the state, the
+            other one is admit it. We find the second behavior more useful, but
+            YMMV. *)
+  ; debug : Debug.t
+        [@default
+          (* Cannot use Debug.none here :-( *)
+          { cache = false
+          ; send = false
+          ; read = false
+          ; lsp_init = false
+          ; parsing = false
+          ; scan = false
+          ; backtraces = false
+          ; unicode = false
+          ; sched_wakeup = false
+          ; request_delay = false
+          ; mem_stats = false
+          ; gc_quick_stats = false
+          }]
+  }
+
+(** Current configuration. *)
+val v : t ref
+
+(** Enable all debug options. *)
+val debug_all : unit -> unit
+
+(** Enable all LSP related debug options. *)
+val debug_lsp : unit -> unit