From 53b6770262a5e40dfe28b8a973b32a58ea3e6f1c 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/init.ml     |  2 +-
 coq/interp.ml   |  2 +-
 coq/parsing.ml  |  2 +-
 coq/print.ml    |  2 +-
 coq/protect.ml  | 27 ++++++++++++++++++++-------
 coq/protect.mli |  2 +-
 coq/state.ml    |  2 +-
 8 files changed, 29 insertions(+), 13 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/init.ml b/coq/init.ml
index 91de9ffbd..65794cd8b 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -85,4 +85,4 @@ let doc_init ~root_state ~workspace ~libname () =
   Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq
 
 let doc_init ~root_state ~workspace ~libname =
-  Protect.eval ~f:(doc_init ~root_state ~workspace ~libname) ()
+  Protect.eval ~pure:true ~f:(doc_init ~root_state ~workspace ~libname) ()
diff --git a/coq/interp.ml b/coq/interp.ml
index f74c84fcc..c7cb12ff9 100644
--- a/coq/interp.ml
+++ b/coq/interp.ml
@@ -27,6 +27,6 @@ let coq_interp ~st cmd =
   Vernacinterp.interp ~st cmd |> State.of_coq
 
 let interp ~st cmd =
-  Protect.eval cmd ~f:(fun cmd ->
+  Protect.eval cmd ~pure:true ~f:(fun cmd ->
       let res = coq_interp ~st cmd in
       { Info.res })
diff --git a/coq/parsing.ml b/coq/parsing.ml
index 933b23845..a8e551a45 100644
--- a/coq/parsing.ml
+++ b/coq/parsing.ml
@@ -9,7 +9,7 @@ let parse ~st ps =
   Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps
   |> Option.map Ast.of_coq
 
-let parse ~st ps = Protect.eval ~f:(parse ~st) ps
+let parse ~st ps = Protect.eval ~pure:false ~f:(parse ~st) ps
 
 (* Read the input stream until a dot or a "end of proof" token is encountered *)
 let parse_to_terminator : unit Pcoq.Entry.t =
diff --git a/coq/print.ml b/coq/print.ml
index ac4bf3a99..3e299d1c3 100644
--- a/coq/print.ml
+++ b/coq/print.ml
@@ -3,4 +3,4 @@ let pr_letype_env ~goal_concl_style env sigma x =
 
 let pr_letype_env ~goal_concl_style env sigma x =
   let f = pr_letype_env ~goal_concl_style env sigma in
-  Protect.eval ~f x
+  Protect.eval ~pure:true ~f x
diff --git a/coq/protect.ml b/coq/protect.ml
index e3cf04c1b..b3a8d622f 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 ~retry 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, retry 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 ~retry:false x in
+      CDebug.set_flags "-backtrace";
+      res
+    | false, _, _ ->
+      R.Completed (Error (User (loc, msg)))
 
 module E = struct
   type 'a t =
@@ -59,8 +72,8 @@ end
 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 eval ~f ~pure x =
+  let r = eval_exn ~retry:pure ~f x in
   let feedback = List.rev !fb_queue in
   let () = fb_queue := [] in
   { E.r; feedback }
diff --git a/coq/protect.mli b/coq/protect.mli
index c477da339..ba0e9182d 100644
--- a/coq/protect.mli
+++ b/coq/protect.mli
@@ -40,4 +40,4 @@ val fb_queue : Message.t list ref
 (** Eval a function and reify the exceptions. Note [f] _must_ be pure, as in
     case of anomaly [f] may be re-executed with debug options. Beware, not
     thread-safe! *)
-val eval : f:('i -> 'o) -> 'i -> 'o E.t
+val eval : f:('i -> 'o) -> pure:bool -> 'i -> 'o E.t
diff --git a/coq/state.ml b/coq/state.ml
index 01ea22a36..e0649eb60 100644
--- a/coq/state.ml
+++ b/coq/state.ml
@@ -96,7 +96,7 @@ let in_state ~st ~f a =
     Vernacstate.unfreeze_interp_state st;
     f a
   in
-  Protect.eval ~f a
+  Protect.eval ~pure:true ~f a
 
 let admit ~st =
   let () = Vernacstate.unfreeze_interp_state st in