From da4399ce1e6178c6ee076f89fdc20f67b599ab6a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 9 Jan 2023 02:09:37 +0100
Subject: [PATCH] [coq] Enable backtraces on anomaly

This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
---
 CHANGES.md     |  3 +++
 coq/protect.ml | 25 +++++++++++++++++++------
 2 files changed, 22 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index c5838dfa6..3a6db03ca 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -4,6 +4,9 @@
  - Support for OCaml 4.11 (@ejgallego, #184)
  - The keybinding alt+enter in VSCode is now correctly scoped
    (@artagnon, #188)
+ - If a command produces an anomaly, coq-lsp will re-execute it with
+   backtracks enabled, as to produce a report (@ejgallego, #161, fixes
+   #153)
 
 # coq-lsp 0.1.3: Event
 ----------------------
diff --git a/coq/protect.ml b/coq/protect.ml
index e3cf04c1b..559d15a0d 100644
--- a/coq/protect.ml
+++ b/coq/protect.ml
@@ -30,18 +30,31 @@ module R = struct
 end
 
 (* Eval and reify exceptions *)
-let eval_exn ~f x =
+let rec eval_exn ~f ~loop x =
   try
     let res = f x in
     R.Completed (Ok res)
   with
   | Sys.Break -> R.Interrupted
   | exn ->
-    let e, info = Exninfo.capture exn in
+    let exn, info = Exninfo.capture exn in
     let loc = Loc.(get_loc info) in
-    let msg = CErrors.iprint (e, info) in
-    if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
-    else R.Completed (Error (User (loc, msg)))
+    let msg = CErrors.iprint (exn, info) in
+    let anomaly = CErrors.is_anomaly exn in
+    let bt = Printexc.backtrace_status () in
+    match anomaly, bt, loop with
+    | true, true, _
+    | true, false, false ->
+      R.Completed (Error (Anomaly (loc, msg)))
+    | true, false, true ->
+      (* This doesn't work because the state unfreeze will restore the
+         "no-backtrace" status *)
+      CDebug.set_flags "backtrace";
+      let res = eval_exn ~f ~loop:false x in
+      CDebug.set_flags "-backtrace";
+      res
+    | false, _, _ ->
+      R.Completed (Error (User (loc, msg)))
 
 module E = struct
   type 'a t =
@@ -60,7 +73,7 @@ let fb_queue : Message.t list ref = ref []
 
 (* Eval with reified exceptions and feedback *)
 let eval ~f x =
-  let r = eval_exn ~f x in
+  let r = eval_exn ~loop:true ~f x in
   let feedback = List.rev !fb_queue in
   let () = fb_queue := [] in
   { E.r; feedback }