From dda75d0b2c75be98a42ad4d8de0f6bd953b407c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 28 Jan 2023 01:00:50 +0100
Subject: [PATCH] [config] Add debug client option.

This is a simpler version of #217

Co-authored-by: Ali Caglayan <alizter@gmail.com>
---
 CHANGES.md                | 2 ++
 controller/coq_lsp.ml     | 1 +
 editor/code/package.json  | 5 +++++
 editor/code/src/config.ts | 7 ++++++-
 fleche/config.ml          | 3 +++
 5 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/CHANGES.md b/CHANGES.md
index a44cf27a..c717bde4 100644
--- a/CHANGES.md
+++ b/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
 ----------------------
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 7a54da22..dc23ee4f 100644
--- a/controller/coq_lsp.ml
+++ b/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
diff --git a/editor/code/package.json b/editor/code/package.json
index 86887d2d..4eb4b643 100644
--- a/editor/code/package.json
+++ b/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",
diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts
index 57e091a4..5e8a6c57 100644
--- a/editor/code/src/config.ts
+++ b/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,
     };
   }
 }
diff --git a/fleche/config.ml b/fleche/config.ml
index db11a4a8..5f5630a3 100644
--- a/fleche/config.ml
+++ b/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