Stream: Coq devs & plugin devs

Topic: Backtrace on anomalies


view this post on Zulip Jason Gross (Sep 06 2022 at 11:13):

I'm getting

Error:
Anomaly
"File "pretyping/evarsolve.ml", line 103, characters 9-15: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Evarsolve.normalize_evar in file "pretyping/evarsolve.ml", line 103, characters 9-21
Called from Evarsolve.invert_definition.imitate in file "pretyping/evarsolve.ml", line 1645, characters 36-58
Called from Stdlib__array.map in file "array.ml", line 106, characters 21-40
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 711, characters 16-34
Called from Stdlib__array.map in file "array.ml", line 108, characters 21-40
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 711, characters 16-34
...

Is there any way to get an Ltac(2) backtrace as well for the anomaly? Set Ltac Backtrace. Set Ltac2 Backtrace. doesn't seem to do it

view this post on Zulip Janno (Sep 06 2022 at 11:27):

It seems likely that the backtrace exists in the exception under Ltac2's let backtrace : backtrace Exninfo.t = Exninfo.make () (defined in tac2entries.ml but not exported). I suspect the challenge would be to let Ltac2 register some kind of hook that would print the Ltac2 backtrace together with the OCaml backtrace. I actually wonder if Exninfo shouldn't generally allow printers to be registered for Exninfo.t fields so that any exception that reaches the user can (optionally) print every field in the exception.

view this post on Zulip Gaëtan Gilbert (Sep 06 2022 at 11:54):

It seems likely that the backtrace exists in the exception

no, I don't think so

view this post on Zulip Janno (Sep 06 2022 at 12:14):

Why not?

view this post on Zulip Janno (Sep 06 2022 at 12:15):

I think with_frame is called on every function call and every call to a primitive so the backtrace should be up to date (assuming Ltac2 Backtrace is enabled)

view this post on Zulip Janno (Sep 06 2022 at 12:20):

Oh, I might be confusing functions here. set_backtrace called by with_frame is for the evarmap field, not for exceptions.

view this post on Zulip Janno (Sep 06 2022 at 12:25):

Yeah the other function is called set_bt and I got confused. Do we just need more set_bt calls in the interpreter?

view this post on Zulip Gaëtan Gilbert (Sep 06 2022 at 12:48):

where would you set_bt for an anomaly?

view this post on Zulip Jason Gross (Sep 06 2022 at 12:52):

(Tangentially, this anomaly seems to have something to do with never calling Constr.check on an evar-containing constr.)

view this post on Zulip Janno (Sep 06 2022 at 12:54):

I don't know how anomalies are handled exactly in Coq. I suspect Coq attaches the OCaml backtrace to the anomaly somehow, or is that from OCaml itself?

view this post on Zulip Gaëtan Gilbert (Sep 06 2022 at 13:10):

raise handles the ocaml backtrace

view this post on Zulip Janno (Sep 06 2022 at 13:58):

Okay, so anomalies are just OCaml exceptions then, right? Why can't we wrap every single Ltac2 step in

try
  <single step>
with
| e ->
  let ie := Exninfo.capture e in
  let info := Exninfo.info ie in
  let info := Exninfo.add info Tac2entries.backtrace  (Option.get (Evd.Store.get (Evd.get_extra_data sigma) Tac2interp.backtrace)) in
  Exninfo.iraise (e, info)

?

view this post on Zulip Janno (Sep 06 2022 at 14:01):

In fact, if that worked, as a first approximation one could print the Ltac2 backtrace directly here. But that assumes the exception is not caught elsewhere so a hook mechanism that prints the Ltac2 backtrace only when the exception escapes still seems better to me


Last updated: Feb 06 2023 at 19:03 UTC