coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Printing the call-stack of coqc on error
- Date: Mon, 28 Jan 2013 07:46:37 -0500
Ah. The main use-case I had in mind was for debugging simple-ish problems in the core of Coq, such as https://coq.inria.fr/bugs/show_bug.cgi?id=2968. In this example, it would be nice to know what line of code initially threw the error that resulted in "The type of this term is a product while it is expected to be ...". Though perhaps what I should actually do is learn to use ocamldebug.
-Jason
On Mon, Jan 28, 2013 at 5:49 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:
No there isn't. Yet.
A few thoughts. Originally that was hard to do because Coq could be compiled with old version of OCaml which didn't have a backtrace support, it's not the case anymore so we could add support for backtraces. Note that Coq needs to be compiled with -g for that to work. Also, there is a high chance that the backtrace be mangled: Coq uses a lot of dynamically loaded plugins, which may cause some issues (I'm not sure), and more importantly, it uses exceptions a lot, with a pretty complex control-flow, and OCaml has a fairly roundabout way to trace errors, which doesn't quite like complex control flows.
On 27 January 2013 21:04, Jason Gross <jasongross9 AT gmail.com> wrote:
Hi,Is there a way to get Coq to print it's (ocaml) call stack whenever it prints "Error: ..."?Thanks.-Jason
- [Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/27/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Arnaud Spiwack, 01/28/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/28/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Pierre-Marie Pédrot, 01/28/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Gabriel Scherer, 01/29/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, AUGER Cédric, 01/29/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/30/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Pierre-Marie Pédrot, 01/30/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Gabriel Scherer, 01/29/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Arnaud Spiwack, 01/28/2013
Archive powered by MHonArc 2.6.18.