Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Printing the call-stack of coqc on error

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Printing the call-stack of coqc on error


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Printing the call-stack of coqc on error
  • Date: Tue, 29 Jan 2013 22:31:08 -0500

Thanks.  Would it be possible to also add it for the Pp.msg_warning case (e.g., for line 37 of kernel/names.ml), for debugging, e.g., https://coq.inria.fr/bugs/show_bug.cgi?id=2956#add_comment?

-Jason

On Mon, Jan 28, 2013 at 8:57 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 27/01/2013 21:04, Jason Gross wrote:
> Is there a way to get Coq to print it's (ocaml) call stack whenever it
> prints "Error: ..."?

I've just added a backtrace printer in the trunk for the [Anomaly] case,
as a proof of concept. I'm not sure whether this is very meaningful in
the [Error] case, because of the many ways it tends to be caught, but I
can also do this indeed.

PMP





Archive powered by MHonArc 2.6.18.

Top of Page