From e8bde450d05908f70ab2c82d9d24f0807c56a94a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 4 Mar 2020 21:39:42 -0500
Subject: [exn] [tactics] improve backtraces on monadic errors

Current backtraces for tactics leave a bit to desire, for example
given the program:

```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```

the backtrace stops at:

```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot  however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.

The backtrace for the failed rewrite is now:

```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

which IMO is much better.
---
 proofs/clenvtac.ml | 4 +++-
 proofs/proof.ml    | 8 ++++++--
 proofs/refine.ml   | 5 ++++-
 3 files changed, 13 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 0257a6f204..007d53f911 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -129,5 +129,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
         Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when CErrors.noncritical e -> Proofview.tclZERO e
+    with e when CErrors.noncritical e ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info e
   end
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 75aca7e7ff..175c487958 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -525,7 +525,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
-    let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+    let nosuchgoal =
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr))
+    in
     let tac = let open Goal_select in match gi with
       | SelectAlreadyFocused ->
         let open Proofview.Notations in
@@ -537,7 +540,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
                Pp.(str "Expected a single focused goal but " ++
                    int n ++ str " goals are focused."))
           in
-          Proofview.tclZERO e
+          let info = Exninfo.reify () in
+          Proofview.tclZERO ~info e
 
       | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
       | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 0bf0cd7b63..a10bbcbdd4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -132,4 +132,7 @@ let solve_constraints =
   tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
    try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
        Unsafe.tclEVARSADVANCE sigma
-   with e -> tclZERO e
+   with e ->
+     (* XXX this is absorbing anomalies? *)
+     let info = Exninfo.reify () in
+     tclZERO ~info e
-- 
cgit v1.2.3