[coq] Enable backtraces on anomaly

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

Fixes #153

CHANGES.md

@@ -1,8 +1,12 @@
-# coq-lsp 0.1.3: 
-------------------------
+# coq-lsp 0.1.3: Prediction
+---------------------------
 
  - Much improved handling of Coq fatal errors, the server is now
-   hardened against them (@ejgallego, #155, #157, #160, fixes #91)
+   hardened against them, and will stop checking on anomalies
+   (@ejgallego, #155, #157, #160, fixes #91)
+ - 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.2: Message
 ------------------------

coq/protect.ml

@@ -29,7 +29,7 @@ module R = struct
     map_error ~f
 end
 
-let eval ~f x =
+let rec eval ~f ~loop x =
   try
     let res = f x in
     R.Completed (Ok res)
@@ -39,5 +39,18 @@ let eval ~f x =
     let e, 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 anomaly = CErrors.is_anomaly e 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 ->
+      CDebug.set_flags "backtrace";
+      let res = eval ~f ~loop:false x in
+      CDebug.set_flags "-backtrace";
+      res
+    | false, _, _ ->
+      R.Completed (Error (User (loc, msg)))
+
+let eval ~f x = eval ~f ~loop:true x