Stream: Coq devs & plugin devs

Topic: ✔ Setting backtrace within coq


view this post on Zulip Ali Caglayan (Nov 10 2021 at 14:19):

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.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2021 at 14:21):

Should be pretty easy, there is the corresponding Printexc.record_backtrace function in OCaml

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 14:21):

Set Debug "backtrace"

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2021 at 14:22):

Aha, that's already implemented, I forgot this is 2021 already

view this post on Zulip Ali Caglayan (Nov 10 2021 at 14:22):

Nice thanks!

view this post on Zulip Notification Bot (Nov 10 2021 at 14:22):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 10 2021 at 14:22):

Ali Caglayan has marked this topic as unresolved.

view this post on Zulip Notification Bot (Nov 10 2021 at 14:22):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Nov 10 2021 at 14:25):

by the way, why do anomalies still print Please report at http://coq.inria.fr/bugs/.? Shouldn't we update this?

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 14:29):

no it works fine


Last updated: Feb 05 2023 at 20:03 UTC