How difficult would it be to have a vernacular command print backtraces? When encountering an anomaly in CoqIDE for instance, it's a bit of a pain to have to restart with -bt
, it would be convenient to be able to tell coq to print it.
Should be pretty easy, there is the corresponding Printexc.record_backtrace function in OCaml
Set Debug "backtrace"
Aha, that's already implemented, I forgot this is 2021 already
Nice thanks!
Ali Caglayan has marked this topic as resolved.
Ali Caglayan has marked this topic as unresolved.
Ali Caglayan has marked this topic as resolved.
by the way, why do anomalies still print Please report at http://coq.inria.fr/bugs/.
? Shouldn't we update this?
no it works fine
Last updated: Oct 13 2024 at 01:02 UTC