[config] Add debug client option.

This is a simpler version of #217

Co-authored-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -19,6 +19,8 @@
    fixes #224)
  - In `_CoqProject`, `-impredicative-set` is now parsed correctly
    (@artagnon, #241)
+ - `debug` option in the client / protocol that will enable Coq's backtraces
+   (@Alizter, @ejgallego, #217, #XXX)
 
 # coq-lsp 0.1.3: Event
 ----------------------

controller/coq_lsp.ml

@@ -281,6 +281,7 @@ let rec lsp_init_loop ic ofmt ~cmdline ~debug : Coq.Workspace.t =
     Rq.answer ~ofmt ~id result;
     LIO.logMessage ~lvl:3 ~message:"Server initialized";
     (* Workspace initialization *)
+    let debug = debug || !Fleche.Config.v.debug in
     let workspace = Coq.Workspace.guess ~cmdline ~debug in
     log_workspace workspace;
     workspace

editor/code/package.json

@@ -143,6 +143,11 @@
             "default": "messages",
             "description": "Traces the communication between VS Code and the language server."
           },
+          "coq-lsp.debug": {
+            "type": "boolean",
+            "default": false,
+            "description": "Enable Debug in Coq Server, usually this will produce backtraces on errors"
+          },
           "coq-lsp.path": {
             "type": "string",
             "default": "coq-lsp",

fleche/config.ml

@@ -21,6 +21,8 @@ type t =
             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 : bool [@default false]
+  (** Enable debug on Coq side, including backtraces *)
   }
 
 let default =
@@ -33,6 +35,7 @@ let default =
   ; show_coq_info_messages = false
   ; show_notices_as_diagnostics = false
   ; admit_on_bad_qed = true
+  ; debug = false
   }
 
 let v = ref default