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. --- doc/changelog/12-misc/11755-exn+tclfail.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/12-misc/11755-exn+tclfail.rst (limited to 'doc') diff --git a/doc/changelog/12-misc/11755-exn+tclfail.rst b/doc/changelog/12-misc/11755-exn+tclfail.rst new file mode 100644 index 0000000000..800cc09e01 --- /dev/null +++ b/doc/changelog/12-misc/11755-exn+tclfail.rst @@ -0,0 +1,4 @@ +- **Added:** + Backtrace information for tactics has been improved + (`#11755 `_, + by Emilio Jesus Gallego Arias). -- cgit v1.2.3