The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

If that can contribute to the discussion, I've been in the situation
of trying to understand where an OCaml exception raised by Coq (due to
an imprudent hack) came from, and it was a painful experience. There
are situations that stash the error backtrace when this could be
avoided (calling an error formatter that internally uses exceptions
for control-flow; this is understandable, but maybe we could set an
option to get the backtrace displayed at this point), and situations
where it seems hard to do so, as Arnaud notes (the various forms of
backtracking used in places I don't know much about).

Agreed, OCaml exceptions should generally not be raised from Coq and
also not be debugged by users (that's what the bugtracker is for), but
any step taken in the direction of a
--something-strange-is-happening-please-try-to-print-the-backtrace
option could still be a win in various situations. I wonder how Coq
developers cope with this issue.

(Granted, the way OCaml collect backtraces does not ease proper
backtrace preservation, but I have no bright idea for a solution that
would incur no additional cost and make everyone happier than with the
current situation.)

On Mon, Jan 28, 2013 at 2:57 PM, 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
>