Enrico Tassi (Nov 15 2021 at 09:37): Enrico Tassi (Nov 15 2021 at 09:37):I'm trying to debug a piece of code that triggers TC resolution. Is there a way to get the tactic backtrace? (the ocaml one is pointless, thanks CPS).
Emilio Jesús Gallego Arias (Nov 15 2021 at 11:21):@Enrico Tassi actually the OCaml one is not too bad, tho still a critical piece is missing? You have an example on how to get the backtrace?
Emilio Jesús Gallego Arias (Nov 15 2021 at 11:21):Does https://github.com/coq/coq/pull/12630 help?
Enrico Tassi (Nov 15 2021 at 11:47):I'm calling an ssr tactic and ssr does not even occur in the trace. The new tactic code is in CPS style, printing the OCaml stack is pointless.
This is what you get by raising an assert false when TC resolution fails (I want to know who calls it):
"File "tactics/class_tactics.ml", line 1094, characters 10-16: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at file "tactics/class_tactics.ml", line 1094, characters 10-21
Called from file "tactics/class_tactics.ml", line 1117, characters 8-130
Called from file "tactics/hints.ml", line 1705, characters 21-51
Called from file "tactics/class_tactics.ml", line 1116, characters 20-209
Called from file "proofs/clenv.ml", line 651, characters 10-126
Called from file "engine/proofview.ml", line 1120, characters 40-46
Called from file "engine/proofview.ml", line 1125, characters 10-34
Called from file "engine/logic_monad.ml", line 192, characters 38-43
Called from file "engine/logic_monad.ml", line 260, characters 6-27
Called from file "engine/proofview.ml", line 233, characters 23-73
Called from file "engine/proofview.ml", line 1263, characters 26-90
Called from file "tactics/tacticals.ml", line 46, characters 16-35
Called from file "clib/cList.ml", line 452, characters 21-26
Called from file "tactics/tacticals.ml", line 82, characters 6-141
Called from file "tactics/tacticals.ml", line 104, characters 13-78
Called from file "engine/proofview.ml", line 1213, characters 10-43
Called from file "engine/evd.ml", line 1448, characters 15-20
Called from file "engine/proofview.ml", line 1225, characters 25-73
Called from file "engine/logic_monad.ml", line 192, characters 38-43
Called from file "engine/logic_monad.ml", line 260, characters 6-27
Called from file "engine/logic_monad.ml", line 260, characters 6-27
Called from file "engine/logic_monad.ml", line 117, characters 8-12
Called from file "engine/proofview.ml", line 234, characters 12-42
Called from file "proofs/proof.ml", line 381, characters 4-49
Called from file "proofs/proof.ml", line 500, characters 31-52
Called from file "vernac/comTactic.ml", line 46, characters 23-59
Called from file "vernac/declare.ml", line 1457, characters 20-33
Called from file "vernac/comTactic.ml", line 43, characters 23-442
Called from file "vernac/vernacextend.ml", line 163, characters 32-47
Called from file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from file "vernac/vernacinterp.ml", line 199, characters 24-69
Called from file "lib/flags.ml", line 17, characters 14-17
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "vernac/vernacinterp.ml", line 249, characters 18-43
Called from file "vernac/vernacinterp.ml", line 247, characters 6-279
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "stm/stm.ml", line 2169, characters 20-47
Called from file "stm/stm.ml", line 2111, characters 10-14
Called from file "stm/stm.ml", line 964, characters 6-10
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "stm/stm.ml", line 2320, characters 4-105
Called from file "stm/stm.ml", line 2421, characters 4-60
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "lib/flags.ml", line 17, characters 14-17
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "toplevel/vernac.ml", line 112, characters 8-69
Called from file "toplevel/vernac.ml", line 116, characters 6-19
Re-raised at file "clib/exninfo.ml", line 81, characters 4-38
Called from file "toplevel/vernac.ml", line 172, characters 30-94
Called from file "toplevel/ccompile.ml", line 146, characters 18-95
Called from file "toplevel/ccompile.ml", line 210, characters 2-59
Called from file "toplevel/coqc.ml", line 47, characters 2-100
Called from file "toplevel/coqc.ml", line 66, characters 4-36
No trace of ssrfwd that is what I'm debugging.
Emilio Jesús Gallego Arias (Nov 15 2021 at 12:32):The monad backtrace and the OCaml backtrace are different, so it depends; there are many places where the OCaml context is lost, but however the OCaml context does provide a lot of info including the toplevel entry point, in tac1 >>> tac2 tac2 is still gonna be in the OCaml context.
Your problem is likely due to some places still dropping the OCaml context.
Emilio Jesús Gallego Arias (Nov 15 2021 at 12:32):We'd need a reproducible example to see what's going on
Last updated: Jun 05 2023 at 10:01 UTC