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: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Printing the call-stack of coqc on error
  • Date: Wed, 30 Jan 2013 12:25:21 +0100

On 30/01/2013 04:31, Jason Gross wrote:
> 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?

I'm afraid no, at least not until this wish is granted:

http://caml.inria.fr/mantis/view.php?id=5899

Currently, we can only inspect the backtrace after an exception was
raise, and as far as I understand, only the part which was unwinded by
the exception. Therefore, you can only get a backtrace whenever an
exception reaches toplevel.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page