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. --- plugins/ltac/rewrite.ml | 38 ++++++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 14 deletions(-) (limited to 'plugins/ltac/rewrite.ml') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index d6b2a17882..4bc8d61258 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1566,7 +1566,8 @@ let assert_replacing id newt tac = Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = - Proofview.tclZERO (Refiner.FailError (n, lazy s)) + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") - | Some None -> if progress then newfail 0 (str"Failed to progress") - else Proofview.tclUNIT () + | Some None -> + if progress + then newfail 0 (str"Failed to progress") + else Proofview.tclUNIT () | Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in @@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let tactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () - with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded") + with e when CErrors.noncritical e -> + let _, info = Exninfo.capture e in + Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = tactic_init_setoid () <*> @@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause = (cl_rewrite_clause_newtac ~progress strat clause) (fun (e, info) -> match e with | RewriteFailure e -> - tclZEROMSG (str"setoid rewrite failed: " ++ e) + tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) - | e -> Proofview.tclZERO ~info e)) + tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) + | e -> + Proofview.tclZERO ~info e)) (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause = @@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) (fun (e, info) -> match e with | RewriteFailure e -> - tclFAIL 0 (str"setoid rewrite failed: " ++ e) + tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) end @@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let not_declared env sigma ty rel = - tclFAIL 0 +let not_declared ~info env sigma ty rel = + tclFAIL ~info 0 (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") @@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback = let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel - with e -> Proofview.tclZERO e + with e -> + (* XXX what is the right test here as to whether e can be converted ? *) + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e end begin function | e -> @@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback = | Hipattern.NoEquationFound -> begin match e with | (Not_found, _) -> - let rel, _, _ = decompose_app_rel env sigma concl in - not_declared env sigma ty rel - | (e, info) -> Proofview.tclZERO ~info e + let rel, _, _ = decompose_app_rel env sigma concl in + not_declared ~info env sigma ty rel + | (e, info) -> + Proofview.tclZERO ~info e end | e' -> Proofview.tclZERO ~info e' end -- cgit v1.2.3