Ali Caglayan (Nov 10 2021 at 14:19): 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.
Pierre-Marie Pédrot (Nov 10 2021 at 14:21):Should be pretty easy, there is the corresponding Printexc.record_backtrace function in OCaml
Gaëtan Gilbert (Nov 10 2021 at 14:21):Set Debug "backtrace"
Pierre-Marie Pédrot (Nov 10 2021 at 14:22):Aha, that's already implemented, I forgot this is 2021 already
Ali Caglayan (Nov 10 2021 at 14:22):Nice thanks!
Notification Bot (Nov 10 2021 at 14:22):Ali Caglayan has marked this topic as resolved.
Notification Bot (Nov 10 2021 at 14:22):Ali Caglayan has marked this topic as unresolved.
Notification Bot (Nov 10 2021 at 14:22):Ali Caglayan has marked this topic as resolved.
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?
Gaëtan Gilbert (Nov 10 2021 at 14:29):no it works fine
Last updated: Apr 18 2024 at 14:02 UTC