Merge pull request #248 from ejgallego/debug_option

[config] Add debug client option.

CHANGES.md

@@ -20,6 +20,8 @@
  - In `_CoqProject`, `-impredicative-set` is now parsed correctly
    (@artagnon, #241)
  - InfoView is not written in React (@ejgallego, #223)
+ - `debug` option in the client / protocol that will enable Coq's backtraces
+   (@Alizter, @ejgallego, #217, #248)
 
 # 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",

editor/code/src/config.ts

@@ -8,10 +8,14 @@ export interface CoqLspServerConfig {
   show_coq_info_messages: boolean;
   show_notices_as_diagnostics: boolean;
   admit_on_bad_qed: boolean;
+  debug: boolean;
 }
 
 export namespace CoqLspServerConfig {
-  export function create(client_version: string, wsConfig: any) {
+  export function create(
+    client_version: string,
+    wsConfig: any
+  ): CoqLspServerConfig {
     return {
       client_version: client_version,
       eager_diagnostics: wsConfig.eager_diagnostics,
@@ -20,6 +24,7 @@ export namespace CoqLspServerConfig {
       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

@@ -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