[coq] Enable backtraces on anomaly

CHANGES.md

@@ -20,6 +20,11 @@
  - In `_CoqProject`, `-impredicative-set` is now parsed correctly
    (@artagnon, #241)
  - InfoView is not written in React (@ejgallego, #223)
+ - 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
+   stack traces enabled, as to produce a better error report
+   (@ejgallego, #161, fixes #153)
 
 # coq-lsp 0.1.3: Event
 ----------------------

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) ()

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 })

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 =

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

coq/protect.ml

@@ -31,18 +31,29 @@ 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
+  | exn -> (
+    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, 'l) t =
@@ -60,8 +71,8 @@ end
 let fb_queue : Loc.t 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 }

coq/protect.mli

@@ -42,4 +42,4 @@ val fb_queue : Loc.t 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, Loc.t) E.t
+val eval : f:('i -> 'o) -> pure:bool -> 'i -> ('o, Loc.t) E.t

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