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
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: Dec 06 2023 at 13:01 UTC