The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Note that in Proofgeneral you can use this flag in a more or less decent way by looking at *coq* buffer and hitting return there. In recent versions of pg (git clone https://github/ProofGeneral/PG) the debugging messages should be displayed in correct buffers.

P.  

Le mardi 1 décembre 2015, James Lottes <jlottes AT gmail.com> a écrit :

Since nobody's mentioned it yet: you can trace through typeclass
resolution interactively with "Set Ltac Debug." in coqtop (though it's
not necessarily obvious which instances/hints are being triggered).
When I get stuck trying to figure out why typeclass resolution isn't
working as I expect, I often resort to pasting my whole development
into coqtop, up to just before the slow command, then "Set Ltac
Debug," followed by the problematic command (a rewrite in your case).
This can be pretty painful, but I haven't found a better way to debug
typeclass resolution.

Cheers,
James

On Mon, Nov 30, 2015 at 9:22 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:
>
> On Nov 30, 2015, at 18:57 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:
>
> Any hints how to analyze the debug log? What should I look for? Here is
> partial log file:
>
> http://bit.ly/1St2sZy
>
>
> Here is a digest of a bigger log file, which shows the search tree:
>
> http://bit.ly/1LK8n6Q
>
>
> Sincerely,
> Vadim Zaliva
>
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> Skype: vzaliva
>