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
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.
It seems likely that the backtrace exists in the exception
no, I don't think so
Why not?
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)
Oh, I might be confusing functions here. set_backtrace
called by with_frame
is for the evarmap field, not for exceptions.
Yeah the other function is called set_bt
and I got confused. Do we just need more set_bt
calls in the interpreter?
where would you set_bt for an anomaly?
(Tangentially, this anomaly seems to have something to do with never calling Constr.check
on an evar-containing constr.)
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?
raise
handles the ocaml backtrace
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)
?
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: Oct 13 2024 at 01:02 UTC